src/Tools/interpretation_with_defs.ML

 
 val _ =
   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)));
 
 end;