diff -r e52e3f697510 -r 8c674b3b8e44 src/CCL/Wfd.thy
--- a/src/CCL/Wfd.thy	Sat Apr 16 16:37:21 2011 +0200
+++ b/src/CCL/Wfd.thy	Sat Apr 16 18:11:20 2011 +0200
@@ -443,9 +443,9 @@
       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
+                    in (nth bvs a, b) end) ihs
       fun try_IHs [] = no_tac
-        | try_IHs ((x,y)::xs) = tac [(("g", 0), x)] (List.nth(rls,y-1)) i ORELSE (try_IHs xs)
+        | try_IHs ((x,y)::xs) = tac [(("g", 0), x)] (nth rls (y - 1)) i ORELSE (try_IHs xs)
   in try_IHs rnames end)
 
 fun is_rigid_prog t =