tuned -- avoid confusion with @{assert} for system failures (exception Fail);
authorwenzelm
Sun Aug 10 15:45:06 2014 +0200 (2014-08-10)
changeset 5788436b5691b81a5
parent 57883 d50aeb916a4b
child 57885 0835aa55ba21
tuned -- avoid confusion with @{assert} for system failures (exception Fail);
src/HOL/Nominal/nominal_inductive.ML
src/HOL/Tools/Datatype/datatype_aux.ML
src/Pure/library.ML
     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));
     2.1 --- a/src/HOL/Tools/Datatype/datatype_aux.ML	Sun Aug 10 15:16:01 2014 +0200
     2.2 +++ b/src/HOL/Tools/Datatype/datatype_aux.ML	Sun Aug 10 15:45:06 2014 +0200
     2.3 @@ -311,10 +311,9 @@
     2.4                else is_nonempty_dt (i :: is) i
     2.5            | arg_nonempty _ = true;
     2.6        in exists (forall (arg_nonempty o strip_dtyp) o snd) constrs end
     2.7 -  in
     2.8 -    assert_all (fn (i, _) => is_nonempty_dt [i] i) (hd descr)
     2.9 -      (fn (_, (s, _, _)) => raise Datatype_Empty s)
    2.10 -  end;
    2.11 +    val _ = hd descr |> forall (fn (i, (s, _, _)) =>
    2.12 +      is_nonempty_dt [i] i orelse raise Datatype_Empty s)
    2.13 +  in () end;
    2.14  
    2.15  (* unfold a list of mutually recursive datatype specifications *)
    2.16  (* all types of the form DtType (dt_name, [..., DtRec _, ...]) *)
     3.1 --- a/src/Pure/library.ML	Sun Aug 10 15:16:01 2014 +0200
     3.2 +++ b/src/Pure/library.ML	Sun Aug 10 15:45:06 2014 +0200
     3.3 @@ -32,7 +32,6 @@
     3.4    exception ERROR of string
     3.5    val error: string -> 'a
     3.6    val cat_error: string -> string -> 'a
     3.7 -  val assert_all: ('a -> bool) -> 'a list -> ('a -> string) -> unit
     3.8  
     3.9    (*pairs*)
    3.10    val pair: 'a -> 'b -> 'a * 'b
    3.11 @@ -269,12 +268,6 @@
    3.12    | cat_error msg "" = error msg
    3.13    | cat_error msg1 msg2 = error (msg1 ^ "\n" ^ msg2);
    3.14  
    3.15 -fun assert_all pred list msg =
    3.16 -  let
    3.17 -    fun ass [] = ()
    3.18 -      | ass (x :: xs) = if pred x then ass xs else error (msg x);
    3.19 -  in ass list end;
    3.20 -
    3.21  
    3.22  (* pairs *)
    3.23