# HG changeset patch
# User bulwahn
# Date 1288034234 -7200
# Node ID 6a53d57fa90276b60c4584aad350b0ba6b1c0746
# Parent  432a776c4aee2e03b0a31a773330f8d3060c9b17
renaming split_modeT' to split_modeT

diff -r 432a776c4aee -r 6a53d57fa902 src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Mon Oct 25 21:17:13 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Mon Oct 25 21:17:14 2010 +0200
@@ -35,7 +35,7 @@
   val split_map_modeT : (mode -> typ -> typ option * typ option)
     -> mode -> typ list -> typ list * typ list
   val split_mode : mode -> term list -> term list * term list
-  val split_modeT' : mode -> typ list -> typ list * typ list
+  val split_modeT : mode -> typ list -> typ list * typ list
   val string_of_mode : mode -> string
   val ascii_string_of_mode : mode -> string
   (* premises *)
@@ -393,24 +393,22 @@
 fun map_filter_prod f (Const (@{const_name Pair}, _) $ t1 $ t2) =
   comb_option HOLogic.mk_prod (map_filter_prod f t1, map_filter_prod f t2)
   | map_filter_prod f t = f t
-
-(* obviously, split_mode' and split_modeT' do not match? where does that cause problems? *)
   
-fun split_modeT' mode Ts =
+fun split_modeT mode Ts =
   let
-    fun split_arg_mode' (Fun _) T = ([], [])
-      | split_arg_mode' (Pair (m1, m2)) (Type (@{type_name Product_Type.prod}, [T1, T2])) =
+    fun split_arg_mode (Fun _) T = ([], [])
+      | split_arg_mode (Pair (m1, m2)) (Type (@{type_name Product_Type.prod}, [T1, T2])) =
         let
-          val (i1, o1) = split_arg_mode' m1 T1
-          val (i2, o2) = split_arg_mode' m2 T2
+          val (i1, o1) = split_arg_mode m1 T1
+          val (i2, o2) = split_arg_mode m2 T2
         in
           (i1 @ i2, o1 @ o2)
         end
-      | split_arg_mode' Input T = ([T], [])
-      | split_arg_mode' Output T = ([], [T])
-      | split_arg_mode' _ _ = raise Fail "split_modeT': mode and type do not match"
+      | split_arg_mode Input T = ([T], [])
+      | split_arg_mode Output T = ([], [T])
+      | split_arg_mode _ _ = raise Fail "split_modeT: mode and type do not match"
   in
-    (pairself flat o split_list) (map2 split_arg_mode' (strip_fun_mode mode) Ts)
+    (pairself flat o split_list) (map2 split_arg_mode (strip_fun_mode mode) Ts)
   end
 
 fun string_of_mode mode =
diff -r 432a776c4aee -r 6a53d57fa902 src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Mon Oct 25 21:17:13 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Mon Oct 25 21:17:14 2010 +0200
@@ -319,7 +319,7 @@
     fn compfuns => fn s => fn T => fn mode => fn additional_arguments => fn compilation =>
     let
       val [depth] = additional_arguments
-      val (_, Ts) = split_modeT' mode (binder_types T)
+      val (_, Ts) = split_modeT mode (binder_types T)
       val T' = mk_predT compfuns (HOLogic.mk_tupleT Ts)
       val if_const = Const (@{const_name "If"}, @{typ bool} --> T' --> T' --> T')
     in