diff --git a/Pantograph/Goal.lean b/Pantograph/Goal.lean
index 7ada190..11e5b20 100644
--- a/Pantograph/Goal.lean
+++ b/Pantograph/Goal.lean
@@ -521,7 +521,7 @@ protected def GoalState.tryMotivatedApply (state: GoalState) (goalId: Nat) (recu
     | .ok syn => pure syn
     | .error error => return .parseError error
   state.execute goalId (tacticM := Tactic.motivatedApply recursor)
-protected def GoalState.tryNoConfusion (state: GoalState) (goalId: Nat) (eq: String):
+protected def GoalState.tryNoConfuse (state: GoalState) (goalId: Nat) (eq: String):
       Elab.TermElabM TacticResult := do
   state.restoreElabM
   let goal ← match state.savedState.tactic.goals.get? goalId with
diff --git a/Pantograph/Library.lean b/Pantograph/Library.lean
index 00b4bc7..608aeeb 100644
--- a/Pantograph/Library.lean
+++ b/Pantograph/Library.lean
@@ -208,5 +208,8 @@ def goalFocus (state: GoalState) (goalId: Nat): Option GoalState :=
 @[export pantograph_goal_motivated_apply_m]
 def goalMotivatedApply (state: GoalState) (goalId: Nat) (recursor: String): Lean.CoreM TacticResult :=
   runTermElabM <| state.tryMotivatedApply goalId recursor
+@[export pantograph_goal_no_confuse_m]
+def goalNoConfuse (state: GoalState) (goalId: Nat) (recursor: String): Lean.CoreM TacticResult :=
+  runTermElabM <| state.tryNoConfuse goalId recursor
 
 end Pantograph