--- a/src/HOL/Nominal/nominal_induct.ML Sat Aug 09 12:28:13 2008 +0200
+++ b/src/HOL/Nominal/nominal_induct.ML Sat Aug 09 22:43:46 2008 +0200
@@ -123,6 +123,8 @@
local
+structure P = OuterParse;
+
val avoidingN = "avoiding";
val fixingN = "arbitrary"; (* to be consistent with induct; hopefully this changes again *)
val ruleN = "rule";
@@ -145,7 +147,7 @@
Scan.repeat (unless_more_args free)) [];
val fixing = Scan.optional (Scan.lift (Args.$$$ fixingN -- Args.colon) |--
- Args.and_list (Scan.repeat (unless_more_args free))) [];
+ P.and_list' (Scan.repeat (unless_more_args free))) [];
val rule_spec = Scan.lift (Args.$$$ "rule" -- Args.colon) |-- Attrib.thms;
@@ -153,7 +155,7 @@
fun nominal_induct_method src =
Method.syntax
- (Args.and_list (Scan.repeat (unless_more_args def_inst)) --
+ (P.and_list' (Scan.repeat (unless_more_args def_inst)) --
avoiding -- fixing -- rule_spec) src
#> (fn ((((x, y), z), w), ctxt) =>
Method.RAW_METHOD_CASES (fn facts =>