src/CCL/Wfd.thy
changeset 29269 5c25a2012975
parent 29264 4ea3358fac3f
child 30510 4120fc59dd85
--- 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 []