renaming split_modeT' to split_modeT
authorbulwahn
Mon Oct 25 21:17:14 2010 +0200 (2010-10-25)
changeset 401396a53d57fa902
parent 40138 432a776c4aee
child 40140 8282b87f957c
renaming split_modeT' to split_modeT
src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
     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 =
     2.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Mon Oct 25 21:17:13 2010 +0200
     2.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Mon Oct 25 21:17:14 2010 +0200
     2.3 @@ -319,7 +319,7 @@
     2.4      fn compfuns => fn s => fn T => fn mode => fn additional_arguments => fn compilation =>
     2.5      let
     2.6        val [depth] = additional_arguments
     2.7 -      val (_, Ts) = split_modeT' mode (binder_types T)
     2.8 +      val (_, Ts) = split_modeT mode (binder_types T)
     2.9        val T' = mk_predT compfuns (HOLogic.mk_tupleT Ts)
    2.10        val if_const = Const (@{const_name "If"}, @{typ bool} --> T' --> T' --> T')
    2.11      in