--- a/src/Pure/thm.ML Wed Dec 13 14:58:49 2023 +0100
+++ b/src/Pure/thm.ML Wed Dec 13 15:23:03 2023 +0100
@@ -2208,11 +2208,12 @@
(* strip_apply f B A strips off all assumptions/parameters from A
introduced by lifting over B, and applies f to remaining part of A*)
fun strip_apply f =
- let fun strip ((c as Const ("Pure.imp", _)) $ _ $ B1)
- (Const ("Pure.imp", _) $ A2 $ B2) = c $ A2 $ strip B1 B2
- | strip ((c as Const ("Pure.all", _)) $ Abs (_, _, t1))
- ( Const ("Pure.all", _) $ Abs (a, T, t2)) = c $ Abs (a, T, strip t1 t2)
- | strip _ A = f A
+ let
+ fun strip ((c as Const ("Pure.imp", _)) $ _ $ B1)
+ (Const ("Pure.imp", _) $ A2 $ B2) = c $ A2 $ strip B1 B2
+ | strip ((c as Const ("Pure.all", _)) $ Abs (_, _, t1))
+ (Const ("Pure.all", _) $ Abs (a, T, t2)) = c $ Abs (a, T, strip t1 t2)
+ | strip _ A = f A
in strip end;
fun strip_lifted (Const ("Pure.imp", _) $ _ $ B1)