outer_params: Syntax.dest_internal;

--- a/src/Pure/drule.ML	Sun Jun 11 21:59:17 2006 +0200
+++ b/src/Pure/drule.ML	Sun Jun 11 21:59:21 2006 +0200
@@ -374,8 +374,8 @@
 fun outer_params t =
   let
     val vs = Term.strip_all_vars t;
-    val xs = Term.variantlist (map (perhaps (try Syntax.dest_skolem) o #1) vs, []);
-  in xs ~~ map #2 vs end;
+    val clean_name = perhaps (try Syntax.dest_skolem) #> perhaps (try Syntax.dest_internal);
+  in Term.variantlist (map (clean_name o #1) vs, []) ~~ map #2 vs end;
 
 (*generalize outermost parameters*)
 fun gen_all th =