src/HOL/Tools/split_rule.ML

--- a/src/HOL/Tools/split_rule.ML	Thu Jun 09 22:25:25 2011 +0200
+++ b/src/HOL/Tools/split_rule.ML	Thu Jun 09 23:12:02 2011 +0200
@@ -73,7 +73,7 @@
         val cterm = Thm.cterm_of (Thm.theory_of_thm rl);
         val (vs', insts) = fold mk_tuple ts (vs, []);
       in
-        (instantiate ([], [(cterm t, cterm newt)] @ insts) rl, vs')
+        (Drule.instantiate_normalize ([], [(cterm t, cterm newt)] @ insts) rl, vs')
       end
   | complete_split_rule_var _ x = x;