--- a/src/HOL/Nominal/nominal_inductive.ML Sun Aug 10 15:16:01 2014 +0200
+++ b/src/HOL/Nominal/nominal_inductive.ML Sun Aug 10 15:45:06 2014 +0200
@@ -167,8 +167,8 @@
val _ = (case duplicates (op = o pairself fst) avoids of
[] => ()
| xs => error ("Duplicate case names: " ^ commas_quote (map fst xs)));
- val _ = assert_all (null o duplicates op = o snd) avoids
- (fn (a, _) => error ("Duplicate variable names for case " ^ quote a));
+ val _ = avoids |> forall (fn (a, xs) => null (duplicates (op =) xs) orelse
+ error ("Duplicate variable names for case " ^ quote a));
val _ = (case subtract (op =) induct_cases (map fst avoids) of
[] => ()
| xs => error ("No such case(s) in inductive definition: " ^ commas_quote xs));