# HG changeset patch
# User wenzelm
# Date 1119025998 -7200
# Node ID e6fedd5baf324b7b0c4832020a89233567555ad2
# Parent  a6e8fb94a8cab032ca36de2915dc17e3b5be27ca
Theory.merge;

diff -r a6e8fb94a8ca -r e6fedd5baf32 src/HOL/Tools/ATP/recon_translate_proof.ML
--- 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