changeset 18375 | 99deeed095ae |
parent 18256 | 8de262a22f23 |
child 18477 | bf2a02c82a55 |
--- a/src/Pure/Isar/rule_cases.ML Thu Dec 08 20:16:04 2005 +0100 +++ b/src/Pure/Isar/rule_cases.ML Thu Dec 08 20:16:10 2005 +0100 @@ -162,7 +162,7 @@ val case_hypsN = "hyps"; val case_premsN = "prems"; -val strip_params = map (apfst Syntax.deskolem) o Logic.strip_params; +val strip_params = map (apfst (perhaps (try Syntax.dest_skolem))) o Logic.strip_params; fun dest_binops cs tm = let