# HG changeset patch
# User wenzelm
# Date 1247686944 -7200
# Node ID fa0cc3c8f73d5e38e7866d8bea540d3b1fbc0cc0
# Parent  a2a3685f61c3cb4690eb7b13982b680fc9304e51
tuned comment;

diff -r a2a3685f61c3 -r fa0cc3c8f73d src/Pure/logic.ML
--- a/src/Pure/logic.ML	Wed Jul 15 20:34:58 2009 +0200
+++ b/src/Pure/logic.ML	Wed Jul 15 21:42:24 2009 +0200
@@ -424,6 +424,8 @@
       a $ Abs(c, T, list_rename_params (cs, t))
   | list_rename_params (cs, B) = B;
 
+
+
 (*** Treatment of "assume", "erule", etc. ***)
 
 (*Strips assumptions in goal yielding
@@ -440,8 +442,7 @@
       strip_assums_imp (nasms-1, H::Hs, B)
   | strip_assums_imp (_, Hs, B) = (Hs, B); (*recursion terminated by B*)
 
-
-(*Strips OUTER parameters only, unlike similar legacy versions.*)
+(*Strips OUTER parameters only.*)
 fun strip_assums_all (params, Const("all",_)$Abs(a,T,t)) =
       strip_assums_all ((a,T)::params, t)
   | strip_assums_all (params, B) = (params, B);