diff -r def4ad161528 -r 4fc9a4fef219 src/Pure/drule.ML
--- a/src/Pure/drule.ML	Tue Jul 11 12:17:01 2006 +0200
+++ b/src/Pure/drule.ML	Tue Jul 11 12:17:02 2006 +0200
@@ -370,10 +370,8 @@
 val forall_elim_vars = PureThy.forall_elim_vars;
 
 fun outer_params t =
-  let
-    val vs = Term.strip_all_vars t;
-    val clean_name = perhaps (try Term.dest_skolem) #> perhaps (try Term.dest_internal);
-  in Term.variantlist (map (clean_name o #1) vs, []) ~~ map #2 vs end;
+  let val vs = Term.strip_all_vars t
+  in Name.variant_list [] (map (Name.clean o #1) vs) ~~ map #2 vs end;
 
 (*generalize outermost parameters*)
 fun gen_all th =
@@ -500,7 +498,7 @@
        [] => (fth, fn x => x)
      | vars =>
          let fun newName (Var(ix,_), (pairs,used)) =
-                   let val v = variant used (string_of_indexname ix)
+                   let val v = Name.variant used (string_of_indexname ix)
                    in  ((ix,v)::pairs, v::used)  end;
              val (alist, _) = foldr newName ([], Library.foldr add_term_names
                (prop :: Thm.terms_of_tpairs tpairs, [])) vars