src/ZF/Tools/cartprod.ML

--- a/src/ZF/Tools/cartprod.ML	Fri Jul 03 16:19:45 2015 +0200
+++ b/src/ZF/Tools/cartprod.ML	Sun Jul 05 15:02:30 2015 +0200
@@ -109,7 +109,7 @@
       in
         remove_split ctxt
           (Drule.instantiate_normalize ([],
-            [apply2 (Thm.cterm_of ctxt) (Var(v, Ind_Syntax.iT-->T2), newt)]) rl)
+            [((v, Ind_Syntax.iT-->T2), Thm.cterm_of ctxt newt)]) rl)
       end
   | split_rule_var _ (t,T,rl) = rl;