src/Pure/Pure.thy
changeset 67777 2d3c1091527b
parent 67764 0f8cb5568b63
child 68276 cbee43ff4ceb
     1.1 --- a/src/Pure/Pure.thy	Tue Mar 06 17:44:19 2018 +0100
     1.2 +++ b/src/Pure/Pure.thy	Tue Mar 06 22:59:00 2018 +0100
     1.3 @@ -617,35 +617,34 @@
     1.4    Outer_Syntax.command \<^command_keyword>\<open>interpret\<close>
     1.5      "prove interpretation of locale expression in proof context"
     1.6      (Parse.!!! Parse_Spec.locale_expression >> (fn expr =>
     1.7 -      Toplevel.proof (Interpretation.interpret_cmd expr [])));
     1.8 +      Toplevel.proof (Interpretation.interpret_cmd expr)));
     1.9  
    1.10  val interpretation_args_with_defs =
    1.11    Parse.!!! Parse_Spec.locale_expression --
    1.12      (Scan.optional (\<^keyword>\<open>defines\<close> |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":"
    1.13 -      -- ((Parse.binding -- Parse.opt_mixfix') --| \<^keyword>\<open>=\<close> -- Parse.term)) >>
    1.14 -      (fn x => (x, []))) ([], []));
    1.15 +      -- ((Parse.binding -- Parse.opt_mixfix') --| \<^keyword>\<open>=\<close> -- Parse.term))) ([]));
    1.16  
    1.17  val _ =
    1.18    Outer_Syntax.local_theory_to_proof \<^command_keyword>\<open>global_interpretation\<close>
    1.19      "prove interpretation of locale expression into global theory"
    1.20 -    (interpretation_args_with_defs >> (fn (expr, (defs, equations)) =>
    1.21 -      Interpretation.global_interpretation_cmd expr defs equations));
    1.22 +    (interpretation_args_with_defs >> (fn (expr, defs) =>
    1.23 +      Interpretation.global_interpretation_cmd expr defs));
    1.24  
    1.25  val _ =
    1.26    Outer_Syntax.command \<^command_keyword>\<open>sublocale\<close>
    1.27      "prove sublocale relation between a locale and a locale expression"
    1.28      ((Parse.position Parse.name --| (\<^keyword>\<open>\<subseteq>\<close> || \<^keyword>\<open><\<close>) --
    1.29 -      interpretation_args_with_defs >> (fn (loc, (expr, (defs, equations))) =>
    1.30 -        Toplevel.theory_to_proof (Interpretation.global_sublocale_cmd loc expr defs equations)))
    1.31 -    || interpretation_args_with_defs >> (fn (expr, (defs, equations)) =>
    1.32 -        Toplevel.local_theory_to_proof NONE NONE (Interpretation.sublocale_cmd expr defs equations)));
    1.33 +      interpretation_args_with_defs >> (fn (loc, (expr, defs)) =>
    1.34 +        Toplevel.theory_to_proof (Interpretation.global_sublocale_cmd loc expr defs)))
    1.35 +    || interpretation_args_with_defs >> (fn (expr, defs) =>
    1.36 +        Toplevel.local_theory_to_proof NONE NONE (Interpretation.sublocale_cmd expr defs)));
    1.37  
    1.38  val _ =
    1.39    Outer_Syntax.command \<^command_keyword>\<open>interpretation\<close>
    1.40      "prove interpretation of locale expression in local theory or into global theory"
    1.41      (Parse.!!! Parse_Spec.locale_expression >> (fn expr =>
    1.42        Toplevel.local_theory_to_proof NONE NONE
    1.43 -        (Interpretation.isar_interpretation_cmd expr [])));
    1.44 +        (Interpretation.isar_interpretation_cmd expr)));
    1.45  
    1.46  in end\<close>
    1.47