src/CCL/Wfd.thy

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