# HG changeset patch
# User wenzelm
# Date 1433006931 -7200
# Node ID 599c4a27785c9ea68871e3e3e286c6fa193b220b
# Parent  932221b62e898e904c1dd7b6dd9209dd0ff3e509
tuned whitespace;

diff -r 932221b62e89 -r 599c4a27785c src/Pure/term.ML
--- a/src/Pure/term.ML	Fri May 29 17:56:43 2015 +0200
+++ b/src/Pure/term.ML	Sat May 30 19:28:51 2015 +0200
@@ -579,13 +579,12 @@
 val propT : typ = Type ("prop",[]);
 
 (* maps  !!x1...xn. t   to   t  *)
-fun strip_all_body (Const("Pure.all",_)$Abs(_,_,t))  =  strip_all_body t
-  | strip_all_body t  =  t;
+fun strip_all_body (Const ("Pure.all", _) $ Abs (_, _, t)) = strip_all_body t
+  | strip_all_body t = t;
 
 (* maps  !!x1...xn. t   to   [x1, ..., xn]  *)
-fun strip_all_vars (Const("Pure.all",_)$Abs(a,T,t))  =
-                (a,T) :: strip_all_vars t
-  | strip_all_vars t  =  [] : (string*typ) list;
+fun strip_all_vars (Const ("Pure.all", _) $ Abs (a, T, t)) = (a, T) :: strip_all_vars t
+  | strip_all_vars t = [];
 
 (*increments a term's non-local bound variables
   required when moving a term within abstractions