src/Tools/interpretation_with_defs.ML
changeset 46949 94aa7b81bcf6
parent 46947 b8c7eb0c2f89
child 46961 5c6955f487e5
--- a/src/Tools/interpretation_with_defs.ML	Thu Mar 15 19:48:19 2012 +0100
+++ b/src/Tools/interpretation_with_defs.ML	Thu Mar 15 20:07:00 2012 +0100
@@ -83,8 +83,8 @@
   Outer_Syntax.command "interpretation"
     "prove interpretation of locale expression in theory" Keyword.thy_goal
     (Parse.!!! (Parse_Spec.locale_expression true) --
-      Scan.optional (Parse.$$$ "defines" |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":"
-        -- ((Parse.binding -- Parse.opt_mixfix') --| Parse.$$$ "is" -- Parse.term))) [] --
+      Scan.optional (@{keyword "defines"} |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":"
+        -- ((Parse.binding -- Parse.opt_mixfix') --| @{keyword "is"} -- Parse.term))) [] --
       Scan.optional (Parse.where_ |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":" -- Parse.prop)) []
       >> (fn ((expr, defs), equations) => Toplevel.print o
           Toplevel.theory_to_proof (interpretation_cmd expr defs equations)));