src/Pure/Isar/isar_syn.ML
changeset 41270 dea60d052923
parent 41249 26f12f98f50a
child 41435 12585dfb86fe
     1.1 --- a/src/Pure/Isar/isar_syn.ML	Sat Dec 18 14:02:14 2010 +0100
     1.2 +++ b/src/Pure/Isar/isar_syn.ML	Sat Dec 18 18:43:13 2010 +0100
     1.3 @@ -414,19 +414,23 @@
     1.4            (begin ? Toplevel.print) o Toplevel.begin_local_theory begin
     1.5              (Expression.add_locale_cmd name Binding.empty expr elems #> snd)));
     1.6  
     1.7 +fun parse_interpretation_arguments mandatory =
     1.8 +  Parse.!!! (Parse_Spec.locale_expression mandatory) --
     1.9 +    Scan.optional
    1.10 +      (Parse.where_ |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":" -- Parse.prop)) [];
    1.11 +
    1.12  val _ =
    1.13    Outer_Syntax.command "sublocale"
    1.14      "prove sublocale relation between a locale and a locale expression" Keyword.thy_goal
    1.15      (Parse.xname --| (Parse.$$$ "\\<subseteq>" || Parse.$$$ "<") --
    1.16 -      Parse.!!! (Parse_Spec.locale_expression false)
    1.17 -      >> (fn (loc, expr) =>
    1.18 -          Toplevel.print o Toplevel.theory_to_proof (Expression.sublocale_cmd loc expr)));
    1.19 +      parse_interpretation_arguments false
    1.20 +      >> (fn (loc, (expr, equations)) =>
    1.21 +          Toplevel.print o Toplevel.theory_to_proof (Expression.sublocale_cmd loc expr equations)));
    1.22  
    1.23  val _ =
    1.24    Outer_Syntax.command "interpretation"
    1.25      "prove interpretation of locale expression in theory" Keyword.thy_goal
    1.26 -    (Parse.!!! (Parse_Spec.locale_expression true) --
    1.27 -      Scan.optional (Parse.where_ |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":" -- Parse.prop)) []
    1.28 +    (parse_interpretation_arguments true
    1.29        >> (fn (expr, equations) => Toplevel.print o
    1.30            Toplevel.theory_to_proof (Expression.interpretation_cmd expr equations)));
    1.31  
    1.32 @@ -434,8 +438,7 @@
    1.33    Outer_Syntax.command "interpret"
    1.34      "prove interpretation of locale expression in proof context"
    1.35      (Keyword.tag_proof Keyword.prf_goal)
    1.36 -    (Parse.!!! (Parse_Spec.locale_expression true) --
    1.37 -      Scan.optional (Parse.where_ |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":" -- Parse.prop)) []
    1.38 +    (parse_interpretation_arguments true
    1.39        >> (fn (expr, equations) => Toplevel.print o
    1.40            Toplevel.proof' (Expression.interpret_cmd expr equations)));
    1.41