src/HOL/Nominal/nominal_inductive.ML
changeset 57884 36b5691b81a5
parent 56253 83b3c110f22d
child 58112 8081087096ad
     1.1 --- a/src/HOL/Nominal/nominal_inductive.ML	Sun Aug 10 15:16:01 2014 +0200
     1.2 +++ b/src/HOL/Nominal/nominal_inductive.ML	Sun Aug 10 15:45:06 2014 +0200
     1.3 @@ -167,8 +167,8 @@
     1.4      val _ = (case duplicates (op = o pairself fst) avoids of
     1.5          [] => ()
     1.6        | xs => error ("Duplicate case names: " ^ commas_quote (map fst xs)));
     1.7 -    val _ = assert_all (null o duplicates op = o snd) avoids
     1.8 -      (fn (a, _) => error ("Duplicate variable names for case " ^ quote a));
     1.9 +    val _ = avoids |> forall (fn (a, xs) => null (duplicates (op =) xs) orelse
    1.10 +      error ("Duplicate variable names for case " ^ quote a));
    1.11      val _ = (case subtract (op =) induct_cases (map fst avoids) of
    1.12          [] => ()
    1.13        | xs => error ("No such case(s) in inductive definition: " ^ commas_quote xs));