--- a/src/CCL/Wfd.thy Wed Dec 31 00:08:14 2008 +0100
+++ b/src/CCL/Wfd.thy Wed Dec 31 15:30:10 2008 +0100
@@ -434,9 +434,9 @@
| get_bno l n (Bound m) = (m-length(l),n)
(* Not a great way of identifying induction hypothesis! *)
-fun could_IH x = could_unify(x,hd (prems_of @{thm rcallT})) orelse
- could_unify(x,hd (prems_of @{thm rcall2T})) orelse
- could_unify(x,hd (prems_of @{thm rcall3T}))
+fun could_IH x = Term.could_unify(x,hd (prems_of @{thm rcallT})) orelse
+ Term.could_unify(x,hd (prems_of @{thm rcall2T})) orelse
+ Term.could_unify(x,hd (prems_of @{thm rcall3T}))
fun IHinst tac rls = SUBGOAL (fn (Bi,i) =>
let val bvs = bvars Bi []