# HG changeset patch
# User chaieb
# Date 1183914090 -7200
# Node ID 4d865f3e4405bc8053e0565498b099b0aeb239b5
# Parent  bccbf6138c30fb0da5bed80ea116f40a4dd31789
Changed syntax for the reflection method (reify unchanged). reflection takes an optional set of theorems for reification then several correctness theorems are specified by rules:'' then the optional term is specified by only:

diff -r bccbf6138c30 -r 4d865f3e4405 src/HOL/ex/Reflection.thy
--- a/src/HOL/ex/Reflection.thy	Sun Jul 08 19:01:28 2007 +0200
+++ b/src/HOL/ex/Reflection.thy	Sun Jul 08 19:01:30 2007 +0200
@@ -21,15 +21,28 @@
 method_setup reify = {*
   fn src =>
     Method.syntax (Attrib.thms --
-      Scan.option (Scan.lift (Args.$$$ "(") |-- Args.term --| Scan.lift (Args.$$$ ")"))) src #>
-  (fn ((eqs, to), ctxt) => Method.SIMPLE_METHOD' (Reflection.genreify_tac ctxt (eqs @ Reify_Data.get ctxt) to))
+      Scan.option (Scan.lift (Args.$$$ "(") |-- Args.term --| Scan.lift (Args.$$$ ")") )) src #>
+  (fn ((eqs, to), ctxt) => Method.SIMPLE_METHOD' (Reflection.genreify_tac ctxt (eqs @ (fst (Reify_Data.get ctxt))) to))
 *} "partial automatic reification"
 
-method_setup reflection = {*
-  fn src =>
-    Method.syntax (Attrib.thms --
-      Scan.option (Scan.lift (Args.$$$ "(") |-- Args.term --| Scan.lift (Args.$$$ ")"))) src #>
-  (fn ((ths, to), ctxt) => Method.SIMPLE_METHOD' (Reflection.reflection_tac ctxt (ths @ Reify_Data.get ctxt) to))
+method_setup reflection = {* 
+let 
+fun keyword k = Scan.lift (Args.$$$ k -- Args.colon) >> K ();
+val onlyN = "only";
+val rulesN = "rules";
+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 Method.SIMPLE_METHOD' (Reflection.reflection_tac ctxt corr_thms raw_eqs to) 
+     end) end
 *} "reflection method"
-
 end