changeset 33317 | b4534348b8fd |
parent 32283 | 3bebc195c124 |
child 36319 | 8feb2c4bef1a |
--- a/src/CCL/Wfd.thy Thu Oct 29 16:59:12 2009 +0100 +++ b/src/CCL/Wfd.thy Thu Oct 29 17:58:26 2009 +0100 @@ -440,7 +440,7 @@ fun IHinst tac rls = SUBGOAL (fn (Bi,i) => let val bvs = bvars Bi [] - val ihs = List.filter could_IH (Logic.strip_assums_hyp Bi) + val ihs = filter could_IH (Logic.strip_assums_hyp Bi) val rnames = map (fn x=> let val (a,b) = get_bno [] 0 x in (List.nth(bvs,a),b) end) ihs