# HG changeset patch
# User wenzelm
# Date 1407678306 -7200
# Node ID 36b5691b81a542f66cf9522d148bc49a83a8df50
# Parent  d50aeb916a4be454fd3c4bc8f9faceaa85f74136
tuned -- avoid confusion with @{assert} for system failures (exception Fail);

diff -r d50aeb916a4b -r 36b5691b81a5 src/HOL/Nominal/nominal_inductive.ML
--- 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));
diff -r d50aeb916a4b -r 36b5691b81a5 src/HOL/Tools/Datatype/datatype_aux.ML
--- a/src/HOL/Tools/Datatype/datatype_aux.ML	Sun Aug 10 15:16:01 2014 +0200
+++ b/src/HOL/Tools/Datatype/datatype_aux.ML	Sun Aug 10 15:45:06 2014 +0200
@@ -311,10 +311,9 @@
               else is_nonempty_dt (i :: is) i
           | arg_nonempty _ = true;
       in exists (forall (arg_nonempty o strip_dtyp) o snd) constrs end
-  in
-    assert_all (fn (i, _) => is_nonempty_dt [i] i) (hd descr)
-      (fn (_, (s, _, _)) => raise Datatype_Empty s)
-  end;
+    val _ = hd descr |> forall (fn (i, (s, _, _)) =>
+      is_nonempty_dt [i] i orelse raise Datatype_Empty s)
+  in () end;
 
 (* unfold a list of mutually recursive datatype specifications *)
 (* all types of the form DtType (dt_name, [..., DtRec _, ...]) *)
diff -r d50aeb916a4b -r 36b5691b81a5 src/Pure/library.ML
--- a/src/Pure/library.ML	Sun Aug 10 15:16:01 2014 +0200
+++ b/src/Pure/library.ML	Sun Aug 10 15:45:06 2014 +0200
@@ -32,7 +32,6 @@
   exception ERROR of string
   val error: string -> 'a
   val cat_error: string -> string -> 'a
-  val assert_all: ('a -> bool) -> 'a list -> ('a -> string) -> unit
 
   (*pairs*)
   val pair: 'a -> 'b -> 'a * 'b
@@ -269,12 +268,6 @@
   | cat_error msg "" = error msg
   | cat_error msg1 msg2 = error (msg1 ^ "\n" ^ msg2);
 
-fun assert_all pred list msg =
-  let
-    fun ass [] = ()
-      | ass (x :: xs) = if pred x then ass xs else error (msg x);
-  in ass list end;
-
 
 (* pairs *)