src/Pure/library.ML
changeset 57884 36b5691b81a5
parent 57831 885888a880fb
child 57909 0fb331032f02
--- 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 *)