--- 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 =
--- 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";
--- 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;
--- 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;