src/Pure/drule.ML
changeset 18375 99deeed095ae
parent 18337 5d24dbd5e93d
child 18468 43951ffb6304
--- a/src/Pure/drule.ML	Thu Dec 08 20:16:04 2005 +0100
+++ b/src/Pure/drule.ML	Thu Dec 08 20:16:10 2005 +0100
@@ -406,7 +406,7 @@
 fun outer_params t =
   let
     val vs = Term.strip_all_vars t;
-    val xs = Term.variantlist (map (Syntax.deskolem o #1) vs, []);
+    val xs = Term.variantlist (map (perhaps (try Syntax.dest_skolem) o #1) vs, []);
   in xs ~~ map #2 vs end;
 
 (*generalize outermost parameters*)