# HG changeset patch
# User wenzelm
# Date 1702477383 -3600
# Node ID 479f31c4b3673f3cc9f006bca21dcd32ed6bb385
# Parent  d33ec0c3672eb6a371d557721dc1c2858c7f18eb
tuned whitespace;

diff -r d33ec0c3672e -r 479f31c4b367 src/Pure/thm.ML
--- 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)