# HG changeset patch
# User wenzelm
# Date 1243680791 -7200
# Node ID 40fa39d9bce7910b8f41b1da131f5c09d7599c36
# Parent  0c5baf034d0e499e32e08393a769518c9f367140
modernized method setup;
tuned;

diff -r 0c5baf034d0e -r 40fa39d9bce7 src/Pure/simplifier.ML
--- a/src/Pure/simplifier.ML	Sat May 30 12:52:57 2009 +0200
+++ b/src/Pure/simplifier.ML	Sat May 30 12:53:11 2009 +0200
@@ -348,16 +348,7 @@
 
 
 
-(** proof methods **)
-
-(* simplification *)
-
-val simp_options =
- (Args.parens (Args.$$$ no_asmN) >> K simp_tac ||
-  Args.parens (Args.$$$ no_asm_simpN) >> K asm_simp_tac ||
-  Args.parens (Args.$$$ no_asm_useN) >> K full_simp_tac ||
-  Args.parens (Args.$$$ asm_lrN) >> K asm_lr_simp_tac ||
-  Scan.succeed asm_full_simp_tac);
+(** method syntax **)
 
 val cong_modifiers =
  [Args.$$$ congN -- Args.colon >> K ((I, cong_add): Method.modifier),
@@ -379,25 +370,33 @@
     >> K (Context.proof_map (map_ss MetaSimplifier.clear_ss), simp_add)]
    @ cong_modifiers;
 
-fun simp_args more_mods =
-  Method.sectioned_args (Args.bang_facts -- Scan.lift simp_options)
-    (more_mods @ simp_modifiers');
+val simp_options =
+ (Args.parens (Args.$$$ no_asmN) >> K simp_tac ||
+  Args.parens (Args.$$$ no_asm_simpN) >> K asm_simp_tac ||
+  Args.parens (Args.$$$ no_asm_useN) >> K full_simp_tac ||
+  Args.parens (Args.$$$ asm_lrN) >> K asm_lr_simp_tac ||
+  Scan.succeed asm_full_simp_tac);
 
-fun simp_method (prems, tac) ctxt = METHOD (fn facts =>
-  ALLGOALS (Method.insert_tac (prems @ facts)) THEN
-    (CHANGED_PROP o ALLGOALS o tac) (local_simpset_of ctxt));
-
-fun simp_method' (prems, tac) ctxt = METHOD (fn facts =>
-  HEADGOAL (Method.insert_tac (prems @ facts) THEN'
-      ((CHANGED_PROP) oo tac) (local_simpset_of ctxt)));
+fun simp_method more_mods meth =
+  Args.bang_facts -- Scan.lift simp_options --|
+    Method.sections (more_mods @ simp_modifiers') >>
+    (fn (prems, tac) => fn ctxt => METHOD (fn facts => meth ctxt tac (prems @ facts)));
 
 
 
 (** setup **)
 
-fun method_setup more_mods = Method.add_methods
- [(simpN, simp_args more_mods simp_method', "simplification"),
-  ("simp_all", simp_args more_mods simp_method, "simplification (all goals)")];
+fun method_setup more_mods =
+  Method.setup (Binding.name simpN)
+    (simp_method more_mods (fn ctxt => fn tac => fn facts =>
+      HEADGOAL (Method.insert_tac facts THEN'
+        (CHANGED_PROP oo tac) (local_simpset_of ctxt))))
+    "simplification" #>
+  Method.setup (Binding.name "simp_all")
+    (simp_method more_mods (fn ctxt => fn tac => fn facts =>
+      ALLGOALS (Method.insert_tac facts) THEN
+        (CHANGED_PROP o ALLGOALS o tac) (local_simpset_of ctxt)))
+    "simplification (all goals)";
 
 fun easy_setup reflect trivs = method_setup [] #> Context.theory_map (map_ss (fn _ =>
   let