# HG changeset patch
# User wenzelm
# Date 1150055961 -7200
# Node ID 04120bdac80e305c762df637167fbaa72f0d429b
# Parent  f2fa72c131864f37c6c2f336c661c5659bded84c
outer_params: Syntax.dest_internal;

diff -r f2fa72c13186 -r 04120bdac80e src/Pure/drule.ML
--- 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 =