src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML
changeset 40139 6a53d57fa902
parent 40101 f7fc517e21c6
child 40844 5895c525739d
     1.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Mon Oct 25 21:17:13 2010 +0200
     1.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Mon Oct 25 21:17:14 2010 +0200
     1.3 @@ -35,7 +35,7 @@
     1.4    val split_map_modeT : (mode -> typ -> typ option * typ option)
     1.5      -> mode -> typ list -> typ list * typ list
     1.6    val split_mode : mode -> term list -> term list * term list
     1.7 -  val split_modeT' : mode -> typ list -> typ list * typ list
     1.8 +  val split_modeT : mode -> typ list -> typ list * typ list
     1.9    val string_of_mode : mode -> string
    1.10    val ascii_string_of_mode : mode -> string
    1.11    (* premises *)
    1.12 @@ -393,24 +393,22 @@
    1.13  fun map_filter_prod f (Const (@{const_name Pair}, _) $ t1 $ t2) =
    1.14    comb_option HOLogic.mk_prod (map_filter_prod f t1, map_filter_prod f t2)
    1.15    | map_filter_prod f t = f t
    1.16 -
    1.17 -(* obviously, split_mode' and split_modeT' do not match? where does that cause problems? *)
    1.18    
    1.19 -fun split_modeT' mode Ts =
    1.20 +fun split_modeT mode Ts =
    1.21    let
    1.22 -    fun split_arg_mode' (Fun _) T = ([], [])
    1.23 -      | split_arg_mode' (Pair (m1, m2)) (Type (@{type_name Product_Type.prod}, [T1, T2])) =
    1.24 +    fun split_arg_mode (Fun _) T = ([], [])
    1.25 +      | split_arg_mode (Pair (m1, m2)) (Type (@{type_name Product_Type.prod}, [T1, T2])) =
    1.26          let
    1.27 -          val (i1, o1) = split_arg_mode' m1 T1
    1.28 -          val (i2, o2) = split_arg_mode' m2 T2
    1.29 +          val (i1, o1) = split_arg_mode m1 T1
    1.30 +          val (i2, o2) = split_arg_mode m2 T2
    1.31          in
    1.32            (i1 @ i2, o1 @ o2)
    1.33          end
    1.34 -      | split_arg_mode' Input T = ([T], [])
    1.35 -      | split_arg_mode' Output T = ([], [T])
    1.36 -      | split_arg_mode' _ _ = raise Fail "split_modeT': mode and type do not match"
    1.37 +      | split_arg_mode Input T = ([T], [])
    1.38 +      | split_arg_mode Output T = ([], [T])
    1.39 +      | split_arg_mode _ _ = raise Fail "split_modeT: mode and type do not match"
    1.40    in
    1.41 -    (pairself flat o split_list) (map2 split_arg_mode' (strip_fun_mode mode) Ts)
    1.42 +    (pairself flat o split_list) (map2 split_arg_mode (strip_fun_mode mode) Ts)
    1.43    end
    1.44  
    1.45  fun string_of_mode mode =