src/Pure/Isar/isar_syn.ML
changeset 40399 a3acca2bddc9
parent 40395 4985aaade799
child 40784 177e8cea3e09
--- a/src/Pure/Isar/isar_syn.ML	Sat Nov 06 20:59:59 2010 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Sun Nov 07 16:39:03 2010 +0100
@@ -502,7 +502,7 @@
   Outer_Syntax.local_theory_to_proof "example_proof"
     "example proof body, without any result" Keyword.thy_schematic_goal
     (Scan.succeed
-      (Specification.schematic_theorem_cmd "" NONE (K I)
+      (Specification.theorem_cmd "" NONE (K I)
         Attrib.empty_binding [] (Element.Shows []) false #> Proof.enter_forward));
 
 val _ =