src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML
changeset 42816 ba14eafef077
parent 42361 23f352990944
child 43324 2b47822868e4
     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