1.1 --- a/src/Pure/Isar/isar_syn.ML	Mon Sep 30 13:59:07 2013 +0200
     1.2 +++ b/src/Pure/Isar/isar_syn.ML	Mon Sep 30 14:04:26 2013 +0200
     1.3 @@ -409,7 +409,7 @@
     1.4            (begin ? Toplevel.print) o Toplevel.begin_local_theory begin
     1.5              (Expression.add_locale_cmd I name Binding.empty expr elems #> snd)));
     1.6  
     1.7 -fun parse_interpretation_arguments mandatory =
     1.8 +fun interpretation_args mandatory =
     1.9    Parse.!!! (Parse_Spec.locale_expression mandatory) --
    1.10      Scan.optional
    1.11        (Parse.where_ |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":" -- Parse.prop)) [];
    1.12 @@ -418,26 +418,26 @@
    1.13    Outer_Syntax.command @{command_spec "sublocale"}
    1.14      "prove sublocale relation between a locale and a locale expression"
    1.15      ((Parse.position Parse.xname --| (@{keyword "\<subseteq>"} || @{keyword "<"}) --
    1.16 -      parse_interpretation_arguments false
    1.17 -      >> (fn (loc, (expr, equations)) =>
    1.18 -          Toplevel.print o Toplevel.theory_to_proof (Expression.sublocale_global_cmd I loc expr equations)))
    1.19 -    || parse_interpretation_arguments false
    1.20 -      >> (fn (expr, equations) => Toplevel.print o
    1.21 -          Toplevel.local_theory_to_proof NONE (Expression.sublocale_cmd expr equations)));
    1.22 +      interpretation_args false >> (fn (loc, (expr, equations)) =>
    1.23 +        Toplevel.print o
    1.24 +        Toplevel.theory_to_proof (Expression.sublocale_global_cmd I loc expr equations)))
    1.25 +    || interpretation_args false >> (fn (expr, equations) =>
    1.26 +        Toplevel.print o
    1.27 +        Toplevel.local_theory_to_proof NONE (Expression.sublocale_cmd expr equations)));
    1.28  
    1.29  val _ =
    1.30    Outer_Syntax.command @{command_spec "interpretation"}
    1.31      "prove interpretation of locale expression in local theory"
    1.32 -    (parse_interpretation_arguments true
    1.33 -      >> (fn (expr, equations) => Toplevel.print o
    1.34 -          Toplevel.local_theory_to_proof NONE (Expression.interpretation_cmd expr equations)));
    1.35 +    (interpretation_args true >> (fn (expr, equations) =>
    1.36 +      Toplevel.print o
    1.37 +      Toplevel.local_theory_to_proof NONE (Expression.interpretation_cmd expr equations)));
    1.38  
    1.39  val _ =
    1.40    Outer_Syntax.command @{command_spec "interpret"}
    1.41      "prove interpretation of locale expression in proof context"
    1.42 -    (parse_interpretation_arguments true
    1.43 -      >> (fn (expr, equations) => Toplevel.print o
    1.44 -          Toplevel.proof' (Expression.interpret_cmd expr equations)));
    1.45 +    (interpretation_args true >> (fn (expr, equations) =>
    1.46 +      Toplevel.print o
    1.47 +      Toplevel.proof' (Expression.interpret_cmd expr equations)));
    1.48  
    1.49  
    1.50  (* classes *)
    1.51 @@ -498,7 +498,7 @@
    1.52  
    1.53  (* statements *)
    1.54  
    1.55 -fun gen_theorem spec schematic kind =
    1.56 +fun theorem spec schematic kind =
    1.57    Outer_Syntax.local_theory_to_proof' spec
    1.58      ("state " ^ (if schematic then "schematic " ^ kind else kind))
    1.59      (Scan.optional (Parse_Spec.opt_thm_name ":" --|
    1.60 @@ -509,12 +509,12 @@
    1.61          ((if schematic then Specification.schematic_theorem_cmd else Specification.theorem_cmd)
    1.62            kind NONE (K I) a includes elems concl)));
    1.63  
    1.64 -val _ = gen_theorem @{command_spec "theorem"} false Thm.theoremK;
    1.65 -val _ = gen_theorem @{command_spec "lemma"} false Thm.lemmaK;
    1.66 -val _ = gen_theorem @{command_spec "corollary"} false Thm.corollaryK;
    1.67 -val _ = gen_theorem @{command_spec "schematic_theorem"} true Thm.theoremK;
    1.68 -val _ = gen_theorem @{command_spec "schematic_lemma"} true Thm.lemmaK;
    1.69 -val _ = gen_theorem @{command_spec "schematic_corollary"} true Thm.corollaryK;
    1.70 +val _ = theorem @{command_spec "theorem"} false Thm.theoremK;
    1.71 +val _ = theorem @{command_spec "lemma"} false Thm.lemmaK;
    1.72 +val _ = theorem @{command_spec "corollary"} false Thm.corollaryK;
    1.73 +val _ = theorem @{command_spec "schematic_theorem"} true Thm.theoremK;
    1.74 +val _ = theorem @{command_spec "schematic_lemma"} true Thm.lemmaK;
    1.75 +val _ = theorem @{command_spec "schematic_corollary"} true Thm.corollaryK;
    1.76  
    1.77  val _ =
    1.78    Outer_Syntax.local_theory_to_proof @{command_spec "notepad"} "begin proof context"
    1.79 @@ -743,8 +743,7 @@
    1.80  
    1.81  val opt_bang = Scan.optional (@{keyword "!"} >> K true) false;
    1.82  
    1.83 -(*Proof General legacy*)
    1.84 -val _ =
    1.85 +val _ = (*Proof General legacy*)
    1.86    Outer_Syntax.improper_command @{command_spec "pretty_setmargin"}
    1.87      "change default margin for pretty printing"
    1.88      (Parse.nat >> (fn n => Toplevel.imperative (fn () => Pretty.margin_default := n)));