# HG changeset patch
# User wenzelm
# Date 1257873083 -3600
# Node ID 4601372337e4cfc9afb5e73679d8923194f49deb
# Parent  35f2b30593a8dcb445ea0d6d2d182a098453c561
eliminated some unused/obsolete Args.bang_facts;

diff -r 35f2b30593a8 -r 4601372337e4 src/HOL/Nominal/nominal_permeq.ML
--- a/src/HOL/Nominal/nominal_permeq.ML	Tue Nov 10 16:04:57 2009 +0100
+++ b/src/HOL/Nominal/nominal_permeq.ML	Tue Nov 10 18:11:23 2009 +0100
@@ -397,11 +397,8 @@
   Scan.succeed (perm_asm_full_simp_tac_i NO_DEBUG_tac));
 
 val perm_simp_meth =
-  Args.bang_facts -- Scan.lift perm_simp_options --|
-  Method.sections (Simplifier.simp_modifiers') >>
-  (fn (prems, tac) => fn ctxt => METHOD (fn facts =>
-    HEADGOAL (Method.insert_tac (prems @ facts) THEN'
-      (CHANGED_PROP oo tac) (simpset_of ctxt))));
+  Scan.lift perm_simp_options --| Method.sections (Simplifier.simp_modifiers') >>
+  (fn tac => fn ctxt => SIMPLE_METHOD' (CHANGED_PROP o tac (simpset_of ctxt)));
 
 (* setup so that the simpset is used which is active at the moment when the tactic is called *)
 fun local_simp_meth_setup tac =
diff -r 35f2b30593a8 -r 4601372337e4 src/HOL/Tools/arith_data.ML
--- a/src/HOL/Tools/arith_data.ML	Tue Nov 10 16:04:57 2009 +0100
+++ b/src/HOL/Tools/arith_data.ML	Tue Nov 10 18:11:23 2009 +0100
@@ -65,8 +65,8 @@
 val setup =
   Arith_Facts.setup #>
   Method.setup @{binding arith}
-    (Args.bang_facts >> (fn prems => fn ctxt =>
-      METHOD (fn facts => HEADGOAL (Method.insert_tac (prems @ get_arith_facts ctxt @ facts)
+    (Scan.succeed (fn ctxt =>
+      METHOD (fn facts => HEADGOAL (Method.insert_tac (get_arith_facts ctxt @ facts)
         THEN' verbose_arith_tac ctxt))))
     "various arithmetic decision procedures";
 
diff -r 35f2b30593a8 -r 4601372337e4 src/HOL/Tools/lin_arith.ML
--- a/src/HOL/Tools/lin_arith.ML	Tue Nov 10 16:04:57 2009 +0100
+++ b/src/HOL/Tools/lin_arith.ML	Tue Nov 10 18:11:23 2009 +0100
@@ -924,9 +924,9 @@
   Attrib.setup @{binding arith_split} (Scan.succeed (Thm.declaration_attribute add_split))
     "declaration of split rules for arithmetic procedure" #>
   Method.setup @{binding linarith}
-    (Args.bang_facts >> (fn prems => fn ctxt =>
+    (Scan.succeed (fn ctxt =>
       METHOD (fn facts =>
-        HEADGOAL (Method.insert_tac (prems @ Arith_Data.get_arith_facts ctxt @ facts)
+        HEADGOAL (Method.insert_tac (Arith_Data.get_arith_facts ctxt @ facts)
           THEN' tac ctxt)))) "linear arithmetic" #>
   Arith_Data.add_tactic "linear arithmetic" gen_tac;
 
diff -r 35f2b30593a8 -r 4601372337e4 src/Tools/intuitionistic.ML
--- a/src/Tools/intuitionistic.ML	Tue Nov 10 16:04:57 2009 +0100
+++ b/src/Tools/intuitionistic.ML	Tue Nov 10 18:11:23 2009 +0100
@@ -87,11 +87,9 @@
 
 fun method_setup name =
   Method.setup name
-    (Args.bang_facts -- Scan.lift (Scan.option OuterParse.nat) --|
-      Method.sections modifiers >>
-      (fn (prems, n) => fn ctxt => METHOD (fn facts =>
-        HEADGOAL (Method.insert_tac (prems @ facts) THEN'
-        ObjectLogic.atomize_prems_tac THEN' prover_tac ctxt n))))
+    (Scan.lift (Scan.option OuterParse.nat) --| Method.sections modifiers >>
+      (fn opt_lim => fn ctxt =>
+        SIMPLE_METHOD' (ObjectLogic.atomize_prems_tac THEN' prover_tac ctxt opt_lim)))
     "intuitionistic proof search";
 
 end;