--- a/src/Tools/interpretation_with_defs.ML Thu Mar 15 17:45:54 2012 +0100
+++ b/src/Tools/interpretation_with_defs.ML Thu Mar 15 19:02:34 2012 +0100
@@ -79,14 +79,11 @@
end;
-val definesK = "defines";
-val _ = Keyword.keyword definesK;
-
val _ =
Outer_Syntax.command "interpretation"
"prove interpretation of locale expression in theory" Keyword.thy_goal
(Parse.!!! (Parse_Spec.locale_expression true) --
- Scan.optional (Parse.$$$ definesK |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":"
+ Scan.optional (Parse.$$$ "defines" |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":"
-- ((Parse.binding -- Parse.opt_mixfix') --| Parse.$$$ "is" -- Parse.term))) [] --
Scan.optional (Parse.where_ |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":" -- Parse.prop)) []
>> (fn ((expr, defs), equations) => Toplevel.print o