--- a/src/HOL/Tools/ATP/recon_translate_proof.ML Fri Jun 17 18:33:17 2005 +0200
+++ b/src/HOL/Tools/ATP/recon_translate_proof.ML Fri Jun 17 18:33:18 2005 +0200
@@ -311,7 +311,7 @@
val mod_lit_th = select_literal (lit2+1) th2
val eqsubst = eq_lit_th RSN (2,rev_subst)
val eq_lit_prem_num = length (prems_of eq_lit_th)
- val sign = Sign.merge (sign_of_thm th1, sign_of_thm th2)
+ val sign = Theory.merge (sign_of_thm th1, sign_of_thm th2)
val newth = Seq.hd (biresolution false [(false, mod_lit_th)] 1 eqsubst)
val newthm = negate_head newth
val newthm' = delete_assumps eq_lit_prem_num newthm