--- a/src/HOL/Library/Reflection.thy Mon Mar 16 17:51:24 2009 +0100
+++ b/src/HOL/Library/Reflection.thy Mon Mar 16 18:24:30 2009 +0100
@@ -16,10 +16,10 @@
use "reflection.ML"
-method_setup reify = {* fn src =>
- Method.syntax (Attrib.thms --
- Scan.option (Scan.lift (Args.$$$ "(") |-- Args.term --| Scan.lift (Args.$$$ ")") )) src #>
- (fn ((eqs, to), ctxt) => SIMPLE_METHOD' (Reflection.genreify_tac ctxt (eqs @ (fst (Reify_Data.get ctxt))) to))
+method_setup reify = {*
+ Attrib.thms --
+ Scan.option (Scan.lift (Args.$$$ "(") |-- Args.term --| Scan.lift (Args.$$$ ")")) >>
+ (fn (eqs, to) => fn ctxt => SIMPLE_METHOD' (Reflection.genreify_tac ctxt (eqs @ (fst (Reify_Data.get ctxt))) to))
*} "partial automatic reification"
method_setup reflection = {*
@@ -30,16 +30,17 @@
val any_keyword = keyword onlyN || keyword rulesN;
val thms = Scan.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat;
val terms = thms >> map (term_of o Drule.dest_term);
- fun optional scan = Scan.optional scan [];
-in fn src =>
- Method.syntax (thms -- optional (keyword rulesN |-- thms) -- Scan.option (keyword onlyN |-- Args.term)) src #>
- (fn (((eqs,ths),to), ctxt) =>
- let
- val (ceqs,cths) = Reify_Data.get ctxt
- val corr_thms = ths@cths
- val raw_eqs = eqs@ceqs
- in SIMPLE_METHOD' (Reflection.reflection_tac ctxt corr_thms raw_eqs to)
- end) end
-*} "reflection method"
+in
+ thms --
+ Scan.optional (keyword rulesN |-- thms) [] --
+ Scan.option (keyword onlyN |-- Args.term) >>
+ (fn ((eqs,ths),to) => fn ctxt =>
+ let
+ val (ceqs,cths) = Reify_Data.get ctxt
+ val corr_thms = ths@cths
+ val raw_eqs = eqs@ceqs
+ in SIMPLE_METHOD' (Reflection.reflection_tac ctxt corr_thms raw_eqs to) end)
+end
+*} "reflection"
end