# HG changeset patch
# User paulson
# Date 1102084092 -3600
# Node ID 05b03ea0f18d45b948af7f48f110974efca38b3b
# Parent  090b16d6c6e04a9189ccf7fdeffb450e7897625d
trying to fix the transfer problem

diff -r 090b16d6c6e0 -r 05b03ea0f18d src/HOL/Tools/res_axioms.ML
--- a/src/HOL/Tools/res_axioms.ML	Fri Dec 03 15:27:47 2004 +0100
+++ b/src/HOL/Tools/res_axioms.ML	Fri Dec 03 15:28:12 2004 +0100
@@ -230,13 +230,13 @@
 
 
 
-(*Transfer a theorem in to theory Hilbert_Choice.thy if it is not already
+(*Transfer a theorem in to theory Reconstruction.thy if it is not already
   inside that theory -- because it's needed for Skolemization *)
 
-val hc_thy = ThyInfo.get_theory"Hilbert_Choice";
+val recon_thy = ThyInfo.get_theory"Reconstruction";
 
-fun transfer_to_Hilbert_Choice thm =
-    transfer hc_thy thm handle THM _ => thm;
+fun transfer_to_Reconstruction thm =
+    transfer recon_thy thm handle THM _ => thm;
 
 (* remove "True" clause *)
 fun rm_redundant_cls [] = []
@@ -249,7 +249,7 @@
 
 (* transform an Isabelle thm into CNF *)
 fun cnf_axiom thm =
-    let val thm' = transfer_to_Hilbert_Choice thm
+    let val thm' = transfer_to_Reconstruction thm
 	val thm'' = if (is_elimR thm') then (cnf_elim thm')
 		    else (if (is_introR thm') then cnf_intro thm' else cnf_rule thm')
     in