# HG changeset patch
# User wenzelm
# Date 1436472500 -7200
# Node ID 6cc14cf3acffdbb2fb19724c5c90a2553d59f719
# Parent  8963331cc0de3beca9c031bcf9d53d5766e90406
tuned whitespace;

diff -r 8963331cc0de -r 6cc14cf3acff src/Pure/logic.ML
--- a/src/Pure/logic.ML	Thu Jul 09 17:36:04 2015 +0200
+++ b/src/Pure/logic.ML	Thu Jul 09 22:08:20 2015 +0200
@@ -452,12 +452,12 @@
 
 (*Strips assumptions in goal, yielding conclusion.   *)
 fun strip_assums_concl (Const("Pure.imp", _) $ H $ B) = strip_assums_concl B
-  | strip_assums_concl (Const("Pure.all",_)$Abs(a,T,t)) = strip_assums_concl t
+  | strip_assums_concl (Const("Pure.all", _) $ Abs (a, T, t)) = strip_assums_concl t
   | strip_assums_concl B = B;
 
 (*Make a list of all the parameters in a subgoal, even if nested*)
 fun strip_params (Const("Pure.imp", _) $ H $ B) = strip_params B
-  | strip_params (Const("Pure.all",_)$Abs(a,T,t)) = (a,T) :: strip_params t
+  | strip_params (Const("Pure.all", _) $ Abs (a, T, t)) = (a, T) :: strip_params t
   | strip_params B = [];
 
 (*test for nested meta connectives in prems*)