--- a/Nominal-General/Nominal2_Eqvt.thy Sun Apr 25 08:18:06 2010 +0200
+++ b/Nominal-General/Nominal2_Eqvt.thy Sun Apr 25 09:13:16 2010 +0200
@@ -287,27 +287,13 @@
use "nominal_permeq.ML"
setup Nominal_Permeq.setup
-ML {*
-val add_thms = Scan.optional (Scan.lift (Args.add -- Args.colon) |-- Attrib.thms) [];
-val exclude_consts = Scan.optional (Scan.lift ((Args.$$$ "exclude") -- Args.colon) |--
- (Scan.repeat (Args.const true))) []
-
-val parser =
- add_thms -- exclude_consts ||
- exclude_consts -- add_thms >> swap
-*}
-
method_setup perm_simp =
- {* parser >>
- (fn (thms, consts) => fn ctxt => SIMPLE_METHOD (HEADGOAL
- (Nominal_Permeq.eqvt_tac ctxt [] consts))) *}
- {* pushes permutations inside *}
+ {* Nominal_Permeq.args_parser >> Nominal_Permeq.perm_simp_meth *}
+ {* pushes permutations inside. *}
method_setup perm_strict_simp =
- {* parser >>
- (fn (thms, consts) => fn ctxt => SIMPLE_METHOD (HEADGOAL
- (Nominal_Permeq.eqvt_strict_tac ctxt thms consts))) *}
- {* pushes permutations inside, raises an error if it cannot solve all permutations *}
+ {* Nominal_Permeq.args_parser >> Nominal_Permeq.perm_strict_simp_meth *}
+ {* pushes permutations inside, raises an error if it cannot solve all permutations. *}
declare [[trace_eqvt = true]]