diff -r a5809fbc939a -r dbd41a84ebd3 src/Pure/Tools/rule_insts.ML
--- a/src/Pure/Tools/rule_insts.ML	Fri Mar 20 20:48:33 2015 +0100
+++ b/src/Pure/Tools/rule_insts.ML	Fri Mar 20 21:16:42 2015 +0100
@@ -231,9 +231,7 @@
     val envT' = map (fn (v, T) => (TVar v, T)) (envT @ Tinsts_env);
     val cenv =
       map (fn ((xi, _), t) => apply2 (Thm.cterm_of ctxt') (Var (xi, fastype_of t), t))
-        (distinct
-          (fn ((x1, t1), (x2, t2)) => x1 = x2 andalso t1 aconv t2)
-          (xis ~~ ts));
+        (xis ~~ ts);
 
 
     (* lift and instantiate rule *)