# HG changeset patch
# User wenzelm
# Date 955630871 -7200
# Node ID 628ffca977b836a35210896ecfaaa42c11d27aa8
# Parent  f93e2dbab86269732790e244af9a87a520433876
added simp_options;
removed emulations of simp_tac etc.;

diff -r f93e2dbab862 -r 628ffca977b8 src/Provers/simplifier.ML
--- a/src/Provers/simplifier.ML	Thu Apr 13 15:00:42 2000 +0200
+++ b/src/Provers/simplifier.ML	Thu Apr 13 15:01:11 2000 +0200
@@ -480,6 +480,12 @@
 
 val colon = Args.$$$ ":";
 
+val simp_options =
+ (Args.$$$ "no_asm" -- colon >> K simp_tac ||
+  Args.$$$ "no_asm_simp" -- colon >> K asm_simp_tac ||
+  Args.$$$ "no_asm_use" -- colon >> K full_simp_tac ||
+  Scan.succeed asm_full_simp_tac);
+
 val simp_modifiers =
  [Args.$$$ simpN -- colon >> K (I, simp_add_local),
   Args.$$$ simpN -- Args.$$$ addN -- colon >> K (I, simp_add_local),
@@ -493,29 +499,23 @@
   Args.$$$ onlyN -- colon >> K (map_local_simpset clear_ss, simp_add_local),
   Args.$$$ otherN -- colon >> K (I, I)];
 
-fun simp_method more_mods tac =
-  (fn prems => fn ctxt => Method.METHOD (fn facts =>
-    ALLGOALS (Method.insert_tac (prems @ facts)) THEN tac (get_local_simpset ctxt)))
-  |> Method.bang_sectioned_args (more_mods @ simp_modifiers');
+fun simp_args more_mods =
+  Method.sectioned_args (Args.bang_facts -- Scan.lift simp_options) (more_mods @ simp_modifiers');
+
 
-fun simp_method' more_mods tac =
-  (fn prems => fn ctxt => Method.METHOD (fn facts =>
-    HEADGOAL (Method.insert_tac (prems @ facts) THEN' tac (get_local_simpset ctxt))))
-  |> Method.bang_sectioned_args (more_mods @ simp_modifiers');
+fun simp_method (prems, tac) ctxt = Method.METHOD (fn facts =>
+  ALLGOALS (Method.insert_tac (prems @ facts)) THEN
+    (CHANGED o ALLGOALS o tac) (get_local_simpset ctxt));
+
+fun simp_method' (prems, tac) ctxt = Method.METHOD (fn facts =>
+  HEADGOAL (Method.insert_tac (prems @ facts) THEN' (CHANGED oo tac) (get_local_simpset ctxt)));
   
 
 (* setup_methods *)
 
 fun setup_methods more_mods = Method.add_methods
- [(simpN,               simp_method' more_mods
-    (CHANGED oo asm_full_simp_tac), "full simplification"),
-  ("simp_all",          simp_method  more_mods (CHANGED o ALLGOALS o asm_full_simp_tac),
-    "full simplification (all goals)"),
-  ("simp_tac",          simp_method' more_mods simp_tac, "simp_tac (improper!)"),
-  ("asm_simp_tac",      simp_method' more_mods asm_simp_tac, "asm_simp_tac (improper!)"),
-  ("full_simp_tac",     simp_method' more_mods full_simp_tac, "full_simp_tac (improper!)"),
-  ("asm_full_simp_tac", simp_method' more_mods asm_full_simp_tac, "asm_full_simp_tac (improper!)"),
-  ("asm_lr_simp_tac",   simp_method' more_mods asm_lr_simp_tac, "asm_lr_simp_tac (improper!)")];
+ [(simpN, simp_args more_mods simp_method', "simplification"),
+  ("simp_all", simp_args more_mods simp_method, "simplification (all goals)")];