# HG changeset patch
# User wenzelm
# Date 1407603039 -7200
# Node ID 4faa0b564a5fece92fb45cb8613bf24e4b70bfd5
# Parent  7d45e47c276513477ed129e3c58043b99ef6acc2
tuned;

diff -r 7d45e47c2765 -r 4faa0b564a5f src/ZF/Tools/datatype_package.ML
--- a/src/ZF/Tools/datatype_package.ML	Sat Aug 09 14:16:46 2014 +0200
+++ b/src/ZF/Tools/datatype_package.ML	Sat Aug 09 18:50:39 2014 +0200
@@ -51,9 +51,9 @@
   FIXME: could insert all constant set expressions, e.g. nat->nat.*)
 fun data_domain co (rec_tms, con_ty_lists) =
     let val rec_hds = map head_of rec_tms
-        val dummy = assert_all is_Const rec_hds
-          (fn t => "Datatype set not previously declared as constant: " ^
-                   Syntax.string_of_term_global @{theory IFOL} t);
+        val dummy = rec_hds |> forall (fn t => is_Const t orelse
+          error ("Datatype set not previously declared as constant: " ^
+                   Syntax.string_of_term_global @{theory IFOL} t));
         val rec_names = (*nat doesn't have to be added*)
             @{const_name nat} :: map (#1 o dest_Const) rec_hds
         val u = if co then @{const QUniv.quniv} else @{const Univ.univ}
@@ -69,9 +69,9 @@
 
   val rec_hds = map head_of rec_tms;
 
-  val dummy = assert_all is_Const rec_hds
-          (fn t => "Datatype set not previously declared as constant: " ^
-                   Syntax.string_of_term_global thy t);
+  val dummy = rec_hds |> forall (fn t => is_Const t orelse
+          error ("Datatype set not previously declared as constant: " ^
+                   Syntax.string_of_term_global thy t));
 
   val rec_names = map (#1 o dest_Const) rec_hds
   val rec_base_names = map Long_Name.base_name rec_names
diff -r 7d45e47c2765 -r 4faa0b564a5f src/ZF/Tools/inductive_package.ML
--- a/src/ZF/Tools/inductive_package.ML	Sat Aug 09 14:16:46 2014 +0200
+++ b/src/ZF/Tools/inductive_package.ML	Sat Aug 09 18:50:39 2014 +0200
@@ -69,31 +69,31 @@
   (*recT and rec_params should agree for all mutually recursive components*)
   val rec_hds = map head_of rec_tms;
 
-  val dummy = assert_all is_Const rec_hds
-          (fn t => "Recursive set not previously declared as constant: " ^
-                   Syntax.string_of_term ctxt t);
+  val dummy = rec_hds |> forall (fn t => is_Const t orelse
+      error ("Recursive set not previously declared as constant: " ^
+                   Syntax.string_of_term ctxt t));
 
   (*Now we know they are all Consts, so get their names, type and params*)
   val rec_names = map (#1 o dest_Const) rec_hds
   and (Const(_,recT),rec_params) = strip_comb (hd rec_tms);
 
   val rec_base_names = map Long_Name.base_name rec_names;
-  val dummy = assert_all Symbol_Pos.is_identifier rec_base_names
-    (fn a => "Base name of recursive set not an identifier: " ^ a);
+  val dummy = rec_base_names |> forall (fn a => Symbol_Pos.is_identifier a orelse
+    error ("Base name of recursive set not an identifier: " ^ a));
 
   local (*Checking the introduction rules*)
     val intr_sets = map (#2 o Ind_Syntax.rule_concl_msg thy) intr_tms;
     fun intr_ok set =
         case head_of set of Const(a,recT) => member (op =) rec_names a | _ => false;
   in
-    val dummy =  assert_all intr_ok intr_sets
-       (fn t => "Conclusion of rule does not name a recursive set: " ^
-                Syntax.string_of_term ctxt t);
+    val dummy = intr_sets |> forall (fn t => intr_ok t orelse
+      error ("Conclusion of rule does not name a recursive set: " ^
+                Syntax.string_of_term ctxt t));
   end;
 
-  val dummy = assert_all is_Free rec_params
-      (fn t => "Param in recursion term not a free variable: " ^
-               Syntax.string_of_term ctxt t);
+  val dummy = rec_params |> forall (fn t => is_Free t orelse
+      error ("Param in recursion term not a free variable: " ^
+               Syntax.string_of_term ctxt t));
 
   (*** Construct the fixedpoint definition ***)
   val mk_variant = singleton (Name.variant_list (List.foldr Misc_Legacy.add_term_names [] intr_tms));