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*)