# HG changeset patch
# User paulson
# Date 865509292 -7200
# Node ID 3e2b8d0de2a07ac5562498520a74e251521615f2
# Parent  aa74c71c39823afd6e6b6ec1712256dd3eef6ef9
Made the pseudo-type of split_rule_var a separate argument

diff -r aa74c71c3982 -r 3e2b8d0de2a0 src/ZF/cartprod.ML
--- a/src/ZF/cartprod.ML	Wed Jun 04 16:03:54 1997 +0200
+++ b/src/ZF/cartprod.ML	Thu Jun 05 13:14:52 1997 +0200
@@ -27,7 +27,7 @@
   val pseudo_type : term -> typ
   val remove_split : thm -> thm
   val split_const : typ -> term
-  val split_rule_var : term * thm -> thm
+  val split_rule_var : term * typ * thm -> thm
   end;
 
 
@@ -75,8 +75,8 @@
 (*Attempts to remove occurrences of split, and pair-valued parameters*)
 val remove_split = rewrite_rule [Pr.split_eq];
 
-(*Uncurries any Var involving pseudo-product type T1 in the rule*)
-fun split_rule_var (t as Var(v, Type("fun",[T1,T2])), rl) =
+(*Uncurries any Var according to its "pseudo-product type" T1 in the rule*)
+fun split_rule_var (Var(v,_), Type("fun",[T1,T2]), rl) =
       let val T' = factors T1 ---> T2
           val newt = ap_split T1 T2 (Var(v,T'))
           val cterm = Thm.cterm_of (#sign(rep_thm rl))
@@ -84,7 +84,7 @@
           remove_split (instantiate ([], [(cterm (Var(v, Ind_Syntax.iT-->T2)), 
                                            cterm newt)]) rl)
       end
-  | split_rule_var (t,rl) = rl;
+  | split_rule_var (t,T,rl) = rl;
 
 end;