--- a/src/FOLP/IFOLP.thy Wed Dec 31 00:08:14 2008 +0100
+++ b/src/FOLP/IFOLP.thy Wed Dec 31 15:30:10 2008 +0100
@@ -1,5 +1,4 @@
(* Title: FOLP/IFOLP.thy
- ID: $Id$
Author: Martin D Coen, Cambridge University Computer Laboratory
Copyright 1992 University of Cambridge
*)
@@ -247,7 +246,7 @@
and concl = discard_proof (Logic.strip_assums_concl prem)
in
if exists (fn hyp => hyp aconv concl) hyps
- then case distinct (op =) (filter (fn hyp => could_unify (hyp, concl)) hyps) of
+ then case distinct (op =) (filter (fn hyp => Term.could_unify (hyp, concl)) hyps) of
[_] => assume_tac i
| _ => no_tac
else no_tac