# 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 *)