# HG changeset patch
# User wenzelm
# Date 1305478767 -7200
# Node ID ba14eafef0775221fdcea5ce8cce99564a79297c
# Parent  61668e617a3bab4f4c5a240f3c7121f4b611e38b
eliminated obsolete "assert" function, including divergent (unused!?) clone in Predicate_Compile_Proof;

diff -r 61668e617a3b -r ba14eafef077 src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Sun May 15 18:00:08 2011 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Sun May 15 18:59:27 2011 +0200
@@ -11,7 +11,6 @@
   val apsnd3 : ('b -> 'd) -> 'a * 'b * 'c -> 'a * 'd * 'c
   val aptrd3 : ('c -> 'd) -> 'a * 'b * 'c -> 'a * 'b * 'd
   val find_indices : ('a -> bool) -> 'a list -> int list
-  val assert : bool -> unit
   (* mode *)
   datatype mode = Bool | Input | Output | Pair of mode * mode | Fun of mode * mode
   val eq_mode : mode * mode -> bool
@@ -189,8 +188,6 @@
 fun find_indices f xs =
   map_filter (fn (i, true) => SOME i | (i, false) => NONE) (map_index (apsnd f) xs)
 
-fun assert check = if check then () else raise Fail "Assertion failed!"
-
 (* mode *)
 
 datatype mode = Bool | Input | Output | Pair of mode * mode | Fun of mode * mode
diff -r 61668e617a3b -r ba14eafef077 src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML	Sun May 15 18:00:08 2011 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML	Sun May 15 18:59:27 2011 +0200
@@ -114,7 +114,7 @@
       | NONE =>
         let
           val (vars, body) = strip_abs t
-          val _ = assert (fastype_of body = body_type (fastype_of body))
+          val _ = @{assert} (fastype_of body = body_type (fastype_of body))
           val absnames = Name.variant_list names (map fst vars)
           val frees = map2 (curry Free) absnames (map snd vars)
           val body' = subst_bounds (rev frees, body)
@@ -212,7 +212,7 @@
           let
             val (f, args) = strip_comb t
             val args = map (Pattern.eta_long []) args
-            val _ = assert (fastype_of t = body_type (fastype_of t))
+            val _ = @{assert} (fastype_of t = body_type (fastype_of t))
             val f' = lookup_pred f
             val Ts = case f' of
               SOME pred => (fst (split_last (binder_types (fastype_of pred))))
@@ -229,7 +229,7 @@
                       if (fastype_of t) = T then t
                       else
                         let
-                          val _ = assert (T =
+                          val _ = @{assert} (T =
                             (binder_types (fastype_of t) @ [@{typ bool}] ---> @{typ bool}))
                           fun mk_if T (b, t, e) =
                             Const (@{const_name If}, @{typ bool} --> T --> T --> T) $ b $ t $ e
diff -r 61668e617a3b -r ba14eafef077 src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML	Sun May 15 18:00:08 2011 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML	Sun May 15 18:59:27 2011 +0200
@@ -98,7 +98,7 @@
           val if_beta = @{lemma "(if c then x else y) z = (if c then x z else y z)" by simp}
           val atom' = Raw_Simplifier.rewrite_term thy
             (map (fn th => th RS @{thm eq_reflection}) [@{thm if_bool_eq_disj}, if_beta]) [] atom
-          val _ = assert (not (atom = atom'))
+          val _ = @{assert} (not (atom = atom'))
         in
           flatten constname atom' (defs, thy)
         end
diff -r 61668e617a3b -r ba14eafef077 src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML	Sun May 15 18:00:08 2011 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML	Sun May 15 18:59:27 2011 +0200
@@ -29,8 +29,6 @@
 
 (** auxiliary **)
 
-fun assert b = if not b then raise Fail "Assertion failed" else warning "Assertion holds"
-
 datatype assertion = Max_number_of_subgoals of int
 fun assert_tac (Max_number_of_subgoals i) st =
   if (nprems_of st <= i) then Seq.single st