src/Pure/Pure.thy
changeset 67764 0f8cb5568b63
parent 67740 b6ce18784872
child 67777 2d3c1091527b
     1.1 --- a/src/Pure/Pure.thy	Sat Mar 03 22:33:25 2018 +0100
     1.2 +++ b/src/Pure/Pure.thy	Sun Mar 04 12:22:48 2018 +0100
     1.3 @@ -622,9 +622,8 @@
     1.4  val interpretation_args_with_defs =
     1.5    Parse.!!! Parse_Spec.locale_expression --
     1.6      (Scan.optional (\<^keyword>\<open>defines\<close> |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":"
     1.7 -      -- ((Parse.binding -- Parse.opt_mixfix') --| \<^keyword>\<open>=\<close> -- Parse.term))
     1.8 -      -- Scan.optional (\<^keyword>\<open>rewrites\<close> |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":"
     1.9 -        -- Parse.prop)) []) ([], []));
    1.10 +      -- ((Parse.binding -- Parse.opt_mixfix') --| \<^keyword>\<open>=\<close> -- Parse.term)) >>
    1.11 +      (fn x => (x, []))) ([], []));
    1.12  
    1.13  val _ =
    1.14    Outer_Syntax.local_theory_to_proof \<^command_keyword>\<open>global_interpretation\<close>