--- a/src/Pure/Isar/attrib.ML Wed Feb 08 09:27:20 2006 +0100
+++ b/src/Pure/Isar/attrib.ML Wed Feb 08 14:39:00 2006 +0100
@@ -253,7 +253,7 @@
fun prepT (a, T) = (Thm.ctyp_of thy (TVar (a, the_sort sorts a)), Thm.ctyp_of thy T);
fun prep (xi, t) = pairself (Thm.cterm_of thy) (Var (xi, Term.fastype_of t), t);
in
- Drule.instantiate (map prepT (distinct envT),
+ Drule.instantiate (map prepT (gen_distinct (op =) envT),
map prep (gen_distinct (fn ((xi, t), (yj, u)) => xi = yj andalso t aconv u) env)) thm
end;