diff --git a/Pantograph/Library.lean b/Pantograph/Library.lean
index fa5d414..3ae852f 100644
--- a/Pantograph/Library.lean
+++ b/Pantograph/Library.lean
@@ -180,6 +180,9 @@ def goalPrint (state: GoalState) (options: @&Protocol.Options): Lean.CoreM Proto
       parent? := ← state.parentExpr?.mapM (λ expr => do
         serializeExpression options (← unfoldAuxLemmas expr)),
     }
+@[export pantograph_goal_diag_m]
+def goalDiag (state: GoalState) (diagOptions: Protocol.GoalDiag) : Lean.CoreM String :=
+  runMetaM $ state.diag diagOptions
 
 @[export pantograph_goal_tactic_m]
 def goalTactic (state: GoalState) (goalId: Nat) (tactic: String): Lean.CoreM TacticResult :=
@@ -212,8 +215,4 @@ def goalMotivatedApply (state: GoalState) (goalId: Nat) (recursor: String): Lean
 def goalNoConfuse (state: GoalState) (goalId: Nat) (eq: String): Lean.CoreM TacticResult :=
   runTermElabM <| state.tryNoConfuse goalId eq
 
-@[export pantograph_goal_diag]
-def goalDiag (state: GoalState) (diagOptions: Protocol.GoalDiag) : Lean.CoreM String :=
-  runMetaM $ state.diag diagOptions
-
 end Pantograph