1.1 --- a/src/Pure/Isar/isar_syn.ML	Sun Dec 05 13:42:58 2010 +0100
     1.2 +++ b/src/Pure/Isar/isar_syn.ML	Sun Dec 05 14:02:16 2010 +0100
     1.3 @@ -513,13 +513,6 @@
     1.4      (Parse.begin >> K Proof.begin_notepad);
     1.5  
     1.6  val _ =
     1.7 -  Outer_Syntax.local_theory_to_proof "example_proof"
     1.8 -    "example proof body, without any result" Keyword.thy_schematic_goal
     1.9 -    (Scan.succeed
    1.10 -      (Specification.theorem_cmd "" NONE (K I)
    1.11 -        Attrib.empty_binding [] (Element.Shows []) false #> Proof.enter_forward));
    1.12 -
    1.13 -val _ =
    1.14    Outer_Syntax.command "have" "state local goal"
    1.15      (Keyword.tag_proof Keyword.prf_goal)
    1.16      (Parse_Spec.statement >> ((Toplevel.print oo Toplevel.proof') o Isar_Cmd.have));