setup for refined facts handling;
Method.bang_sectioned_args / Args.bang_facts;
eliminated asm_simp;
tuned improper methods;

--- a/src/Provers/simplifier.ML	Tue Sep 21 17:24:50 1999 +0200
+++ b/src/Provers/simplifier.ML	Tue Sep 21 17:26:42 1999 +0200
@@ -417,7 +417,6 @@
 (* add / del *)
 
 val simpN = "simp";
-val asm_simpN = "asm_simp";
 val addN = "add";
 val delN = "del";
 val onlyN = "only";
@@ -468,29 +467,21 @@
   Args.$$$ onlyN >> K (map_local_simpset clear_ss, simp_add_local),
   Args.$$$ otherN >> K (I, I)];
 
-val simp_args = Method.only_sectioned_args simp_modifiers';
-
-fun simp_meth thin cut tac ctxt = Method.METHOD (fn facts =>
-  FIRSTGOAL
-    ((if thin then REPEAT_DETERM o etac Drule.thin_rl else K all_tac)
-      THEN' (if cut then Method.insert_tac facts else K all_tac)
-      THEN' tac (get_local_simpset ctxt)));
-
-val simp_method = simp_args ooo simp_meth;
+fun simp_method tac =
+  (fn prems => fn ctxt => Method.METHOD (fn facts =>
+    FIRSTGOAL (Method.insert_tac (prems @ facts) THEN' tac (get_local_simpset ctxt))))
+  |> Method.bang_sectioned_args simp_modifiers';
 
 
 (* setup_methods *)
 
 val setup_methods = Method.add_methods
- [(simpN,               simp_method true true (CHANGED oo asm_full_simp_tac),
-    "full simplification (including facts, excluding assumptions)"),
-  (asm_simpN,           simp_method false true (CHANGED oo asm_full_simp_tac),
-    "full simplification (including facts and assumptions)"),
-  ("simp_tac",          simp_method false false simp_tac, "simp_tac (improper!)"),
-  ("asm_simp_tac",      simp_method false false asm_simp_tac, "asm_simp_tac (improper!)"),
-  ("full_simp_tac",     simp_method false false full_simp_tac, "full_simp_tac (improper!)"),
-  ("asm_full_simp_tac", simp_method false false asm_full_simp_tac, "asm_full_simp_tac (improper!)"),
-  ("asm_lr_simp_tac",   simp_method false false asm_lr_simp_tac, "asm_lr_simp_tac (improper!)")];
+ [(simpN,               simp_method (CHANGED oo asm_full_simp_tac), "full simplification"),
+  ("simp_tac",          simp_method simp_tac, "simp_tac (improper!)"),
+  ("asm_simp_tac",      simp_method asm_simp_tac, "asm_simp_tac (improper!)"),
+  ("full_simp_tac",     simp_method full_simp_tac, "full_simp_tac (improper!)"),
+  ("asm_full_simp_tac", simp_method asm_full_simp_tac, "asm_full_simp_tac (improper!)"),
+  ("asm_lr_simp_tac",   simp_method asm_lr_simp_tac, "asm_lr_simp_tac (improper!)")];