Theory.merge;
authorwenzelm
Fri Jun 17 18:33:18 2005 +0200 (2005-06-17)
changeset 16433e6fedd5baf32
parent 16432 a6e8fb94a8ca
child 16434 d17817dd61e9
Theory.merge;
src/HOL/Tools/ATP/recon_translate_proof.ML
     1.1 --- a/src/HOL/Tools/ATP/recon_translate_proof.ML	Fri Jun 17 18:33:17 2005 +0200
     1.2 +++ b/src/HOL/Tools/ATP/recon_translate_proof.ML	Fri Jun 17 18:33:18 2005 +0200
     1.3 @@ -311,7 +311,7 @@
     1.4  	  val mod_lit_th = select_literal (lit2+1) th2
     1.5  	  val eqsubst = eq_lit_th RSN (2,rev_subst)
     1.6  	  val eq_lit_prem_num = length (prems_of eq_lit_th)
     1.7 -	  val sign = Sign.merge (sign_of_thm th1, sign_of_thm th2)
     1.8 +	  val sign = Theory.merge (sign_of_thm th1, sign_of_thm th2)
     1.9  	  val newth = Seq.hd (biresolution false [(false, mod_lit_th)] 1 eqsubst)
    1.10       	  val newthm = negate_head newth
    1.11  	  val newthm' = delete_assumps eq_lit_prem_num newthm