--- 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 =