Repaired strip_assums_hyp (now also works for goals not
authorberghofe
Fri, 13 Oct 2006 18:08:48 +0200
changeset 21016 430b35c9cd27
parent 21015 425883e01fe0
child 21017 5693e4471c2b
Repaired strip_assums_hyp (now also works for goals not in hhf normal form).
src/Pure/logic.ML
--- a/src/Pure/logic.ML	Fri Oct 13 16:52:51 2006 +0200
+++ b/src/Pure/logic.ML	Fri Oct 13 18:08:48 2006 +0200
@@ -424,9 +424,13 @@
   in lift [] end;
 
 (*Strips assumptions in goal, yielding list of hypotheses.   *)
-fun strip_assums_hyp (Const("==>", _) $ H $ B) = H :: strip_assums_hyp B
-  | strip_assums_hyp (Const("all",_)$Abs(a,T,t)) = strip_assums_hyp t
-  | strip_assums_hyp B = [];
+fun strip_assums_hyp B =
+  let
+    fun strip Hs (Const ("==>", _) $ H $ B) = strip (H :: Hs) B
+      | strip Hs (Const ("all", _) $ Abs (a, T, t)) =
+          strip (map (incr_boundvars 1) Hs) t
+      | strip Hs B = rev Hs
+  in strip [] B end;
 
 (*Strips assumptions in goal, yielding conclusion.   *)
 fun strip_assums_concl (Const("==>", _) $ H $ B) = strip_assums_concl B