eliminated obsolete "assert" function, including divergent (unused!?) clone in Predicate_Compile_Proof;
authorwenzelm
Sun May 15 18:59:27 2011 +0200 (2011-05-15)
changeset 42816ba14eafef077
parent 42815 61668e617a3b
child 42817 7e819eb7dabb
eliminated obsolete "assert" function, including divergent (unused!?) clone in Predicate_Compile_Proof;
src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML
     1.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Sun May 15 18:00:08 2011 +0200
     1.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Sun May 15 18:59:27 2011 +0200
     1.3 @@ -11,7 +11,6 @@
     1.4    val apsnd3 : ('b -> 'd) -> 'a * 'b * 'c -> 'a * 'd * 'c
     1.5    val aptrd3 : ('c -> 'd) -> 'a * 'b * 'c -> 'a * 'b * 'd
     1.6    val find_indices : ('a -> bool) -> 'a list -> int list
     1.7 -  val assert : bool -> unit
     1.8    (* mode *)
     1.9    datatype mode = Bool | Input | Output | Pair of mode * mode | Fun of mode * mode
    1.10    val eq_mode : mode * mode -> bool
    1.11 @@ -189,8 +188,6 @@
    1.12  fun find_indices f xs =
    1.13    map_filter (fn (i, true) => SOME i | (i, false) => NONE) (map_index (apsnd f) xs)
    1.14  
    1.15 -fun assert check = if check then () else raise Fail "Assertion failed!"
    1.16 -
    1.17  (* mode *)
    1.18  
    1.19  datatype mode = Bool | Input | Output | Pair of mode * mode | Fun of mode * mode
     2.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML	Sun May 15 18:00:08 2011 +0200
     2.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML	Sun May 15 18:59:27 2011 +0200
     2.3 @@ -114,7 +114,7 @@
     2.4        | NONE =>
     2.5          let
     2.6            val (vars, body) = strip_abs t
     2.7 -          val _ = assert (fastype_of body = body_type (fastype_of body))
     2.8 +          val _ = @{assert} (fastype_of body = body_type (fastype_of body))
     2.9            val absnames = Name.variant_list names (map fst vars)
    2.10            val frees = map2 (curry Free) absnames (map snd vars)
    2.11            val body' = subst_bounds (rev frees, body)
    2.12 @@ -212,7 +212,7 @@
    2.13            let
    2.14              val (f, args) = strip_comb t
    2.15              val args = map (Pattern.eta_long []) args
    2.16 -            val _ = assert (fastype_of t = body_type (fastype_of t))
    2.17 +            val _ = @{assert} (fastype_of t = body_type (fastype_of t))
    2.18              val f' = lookup_pred f
    2.19              val Ts = case f' of
    2.20                SOME pred => (fst (split_last (binder_types (fastype_of pred))))
    2.21 @@ -229,7 +229,7 @@
    2.22                        if (fastype_of t) = T then t
    2.23                        else
    2.24                          let
    2.25 -                          val _ = assert (T =
    2.26 +                          val _ = @{assert} (T =
    2.27                              (binder_types (fastype_of t) @ [@{typ bool}] ---> @{typ bool}))
    2.28                            fun mk_if T (b, t, e) =
    2.29                              Const (@{const_name If}, @{typ bool} --> T --> T --> T) $ b $ t $ e
     3.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML	Sun May 15 18:00:08 2011 +0200
     3.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML	Sun May 15 18:59:27 2011 +0200
     3.3 @@ -98,7 +98,7 @@
     3.4            val if_beta = @{lemma "(if c then x else y) z = (if c then x z else y z)" by simp}
     3.5            val atom' = Raw_Simplifier.rewrite_term thy
     3.6              (map (fn th => th RS @{thm eq_reflection}) [@{thm if_bool_eq_disj}, if_beta]) [] atom
     3.7 -          val _ = assert (not (atom = atom'))
     3.8 +          val _ = @{assert} (not (atom = atom'))
     3.9          in
    3.10            flatten constname atom' (defs, thy)
    3.11          end
     4.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML	Sun May 15 18:00:08 2011 +0200
     4.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML	Sun May 15 18:59:27 2011 +0200
     4.3 @@ -29,8 +29,6 @@
     4.4  
     4.5  (** auxiliary **)
     4.6  
     4.7 -fun assert b = if not b then raise Fail "Assertion failed" else warning "Assertion holds"
     4.8 -
     4.9  datatype assertion = Max_number_of_subgoals of int
    4.10  fun assert_tac (Max_number_of_subgoals i) st =
    4.11    if (nprems_of st <= i) then Seq.single st