--- 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