1.1 --- a/src/Pure/Pure.thy	Wed Feb 03 16:39:44 2021 +0100
     1.2 +++ b/src/Pure/Pure.thy	Thu Feb 11 17:45:29 2021 +0100
     1.3 @@ -497,7 +497,7 @@
     1.4  subsubsection \<open>Theorems\<close>
     1.5  
     1.6  ML \<open>
     1.7 -local
     1.8 +(**)local(**)
     1.9  
    1.10  val long_keyword =
    1.11    Parse_Spec.includes >> K "" ||
    1.12 @@ -526,7 +526,7 @@
    1.13  val _ = theorem \<^command_keyword>\<open>proposition\<close> false "proposition";
    1.14  val _ = theorem \<^command_keyword>\<open>schematic_goal\<close> true "schematic goal";
    1.15  
    1.16 -in end\<close>
    1.17 +(**)in end(**)\<close>
    1.18  
    1.19  ML \<open>
    1.20  local
    1.21 @@ -1418,6 +1418,56 @@
    1.22  
    1.23  in end\<close>
    1.24  
    1.25 +ML \<open> (** types of **)
    1.26 +\<close> text \<open> (*prep.for theorem: outcomment (** )local( **) above!*)
    1.27 +long_statement:
    1.28 +  Token.T list -> (bool * Attrib.binding * (xstring * Position.T) list * Element.context list * Element.statement) * Token.T list
    1.29 +\<close> text \<open>
    1.30 +short_statement:
    1.31 +  Token.T list -> (bool * (binding * _d list) * _c list * (string, string, _b) Element.ctxt list * (_a, string) Element.stmt) * Token.T list
    1.32 +\<close> text \<open>
    1.33 +fun theorem spec schematic descr =
    1.34 +  Outer_Syntax.local_theory_to_proof' spec ("state " ^ descr)
    1.35 +    ((long_statement || (*short_statement*)long_statement) >> (fn (long, binding, includes, elems, concl) =>
    1.36 +      ((if schematic then Specification.schematic_theorem_cmd else Specification.theorem_cmd)
    1.37 +        long Thm.theoremK NONE (K I) binding includes elems concl)) );
    1.38 +\<close> text \<open>
    1.39 +theorem: Outer_Syntax.command_keyword -> bool -> string -> unit;
    1.40 +val schematic = false;
    1.41 +\<close> ML \<open>
    1.42 +\<close> text \<open> (*Outer_Syntax.local_theory_to_proof' ...    :: thy_goal_stmt*)
    1.43 +(fn (long, binding, includes, elems, concl) =>
    1.44 +      ((if schematic then Specification.schematic_theorem_cmd else Specification.theorem_cmd)
    1.45 +        long Thm.theoremK NONE (K I) binding includes elems concl))
    1.46 +: 
    1.47 +  bool * Attrib.binding * (xstring * Position.T) list * Element.context list * Element.statement -> bool ->
    1.48 +    local_theory(*Proof.context*) -> Proof.state
    1.49 +(*  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^    ^^^^^^^^^^^*)
    1.50 +\<close> ML \<open>
    1.51 +\<close> ML \<open> (*Outer_Syntax.command \<^command_keyword>\<open>from\<close>  :: prf_chain % "proof" *)
    1.52 +Toplevel.proof o Proof.from_thmss_cmd:
    1.53 +  (Facts.ref * Token.src list) list list -> Toplevel.transition -> Toplevel.transition
    1.54 +(*                                          ^^^^^^^^^^^^^^^^^^^    ^^^^^^^^^^^^^^^^^^^*)
    1.55 +\<close> ML \<open>
    1.56 +\<close> ML \<open> (**)
    1.57 +\<close> ML \<open>
    1.58 +\<close> ML \<open> (**)
    1.59 +\<close> ML \<open>
    1.60 +\<close> ML \<open> (**)
    1.61 +\<close> ML \<open>
    1.62 +\<close> ML \<open> (**)
    1.63 +\<close> ML \<open>
    1.64 +\<close> ML \<open> (**)
    1.65 +\<close> ML \<open>
    1.66 +\<close> ML \<open> (**)
    1.67 +\<close> ML \<open>
    1.68 +\<close> ML \<open> (**)
    1.69 +\<close> ML \<open>
    1.70 +\<close> ML \<open> (**)
    1.71 +\<close> ML \<open>
    1.72 +\<close> ML \<open>
    1.73 +\<close>
    1.74 +
    1.75  
    1.76  section \<open>Auxiliary lemmas\<close>
    1.77