diff -r 75786c2eb897 -r bc5c6c9b114e src/Pure/Isar/method.ML
--- a/src/Pure/Isar/method.ML	Wed Feb 15 19:11:10 2006 +0100
+++ b/src/Pure/Isar/method.ML	Wed Feb 15 21:34:55 2006 +0100
@@ -290,7 +290,7 @@
 
 val remdups_tac = SUBGOAL (fn (g, i) =>
   let val prems = Logic.strip_assums_hyp g in
-    REPEAT_DETERM_N (length prems - length (gen_distinct op aconv prems))
+    REPEAT_DETERM_N (length prems - length (distinct op aconv prems))
     (Tactic.ematch_tac [Drule.remdups_rl] i THEN Tactic.eq_assume_tac i)
   end);
 
@@ -393,7 +393,7 @@
           map
             (fn (xi, t) =>
               pairself (Thm.cterm_of thy) (Var (xi, fastype_of t), t))
-            (gen_distinct
+            (distinct
               (fn ((x1, t1), (x2, t2)) => x1 = x2 andalso t1 aconv t2)
               (xis ~~ ts));
         (* Lift and instantiate rule *)