src/Pure/Isar/isar_syn.ML
changeset 36317 506d732cb522
parent 36178 0e5c133b48b6
child 36323 655e2d74de3a
     1.1 --- a/src/Pure/Isar/isar_syn.ML	Fri Apr 23 22:39:49 2010 +0200
     1.2 +++ b/src/Pure/Isar/isar_syn.ML	Fri Apr 23 22:48:07 2010 +0200
     1.3 @@ -491,16 +491,23 @@
     1.4  
     1.5  (* statements *)
     1.6  
     1.7 -fun gen_theorem kind =
     1.8 -  OuterSyntax.local_theory_to_proof' kind ("state " ^ kind) K.thy_goal
     1.9 +fun gen_theorem schematic kind =
    1.10 +  OuterSyntax.local_theory_to_proof'
    1.11 +    (if schematic then "schematic_" ^ kind else kind)
    1.12 +    ("state " ^ (if schematic then "schematic " ^ kind else kind))
    1.13 +    (if schematic then K.thy_schematic_goal else K.thy_goal)
    1.14      (Scan.optional (SpecParse.opt_thm_name ":" --|
    1.15        Scan.ahead (SpecParse.locale_keyword || SpecParse.statement_keyword)) Attrib.empty_binding --
    1.16        SpecParse.general_statement >> (fn (a, (elems, concl)) =>
    1.17 -        (Specification.theorem_cmd kind NONE (K I) a elems concl)));
    1.18 +        ((if schematic then Specification.schematic_theorem_cmd else Specification.theorem_cmd)
    1.19 +          kind NONE (K I) a elems concl)));
    1.20  
    1.21 -val _ = gen_theorem Thm.theoremK;
    1.22 -val _ = gen_theorem Thm.lemmaK;
    1.23 -val _ = gen_theorem Thm.corollaryK;
    1.24 +val _ = gen_theorem false Thm.theoremK;
    1.25 +val _ = gen_theorem false Thm.lemmaK;
    1.26 +val _ = gen_theorem false Thm.corollaryK;
    1.27 +val _ = gen_theorem true Thm.theoremK;
    1.28 +val _ = gen_theorem true Thm.lemmaK;
    1.29 +val _ = gen_theorem true Thm.corollaryK;
    1.30  
    1.31  val _ =
    1.32    OuterSyntax.command "have" "state local goal"