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