src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML
changeset 59057 5b649fb2f2e1
parent 57962 0284a7d083be
child 59058 a78612c67ec0
     1.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Wed Nov 26 15:44:32 2014 +0100
     1.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Wed Nov 26 16:55:43 2014 +0100
     1.3 @@ -6,10 +6,6 @@
     1.4  
     1.5  signature PREDICATE_COMPILE_AUX =
     1.6  sig
     1.7 -  (* general functions *)
     1.8 -  val apfst3 : ('a -> 'd) -> 'a * 'b * 'c -> 'd * 'b * 'c
     1.9 -  val apsnd3 : ('b -> 'd) -> 'a * 'b * 'c -> 'a * 'd * 'c
    1.10 -  val aptrd3 : ('c -> 'd) -> 'a * 'b * 'c -> 'a * 'b * 'd
    1.11    val find_indices : ('a -> bool) -> 'a list -> int list
    1.12    (* mode *)
    1.13    datatype mode = Bool | Input | Output | Pair of mode * mode | Fun of mode * mode
    1.14 @@ -172,10 +168,6 @@
    1.15  
    1.16  (* general functions *)
    1.17  
    1.18 -fun apfst3 f (x, y, z) = (f x, y, z)
    1.19 -fun apsnd3 f (x, y, z) = (x, f y, z)
    1.20 -fun aptrd3 f (x, y, z) = (x, y, f z)
    1.21 -
    1.22  fun comb_option f (SOME x1, SOME x2) = SOME (f (x1, x2))
    1.23    | comb_option f (NONE, SOME x2) = SOME x2
    1.24    | comb_option f (SOME x1, NONE) = SOME x1