# HG changeset patch
# User berghofe
# Date 1160755728 -7200
# Node ID 430b35c9cd27e92c77f186f2d31daaed716e0da6
# Parent  425883e01fe0fb252da9c973f060682d298cd63c
Repaired strip_assums_hyp (now also works for goals not
in hhf normal form).

diff -r 425883e01fe0 -r 430b35c9cd27 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