# HG changeset patch
# User obua
# Date 1127499234 -7200
# Node ID 7725da65f8e03c09ecae7fda8b8a54f4da04c436
# Parent  6527ba893bae769a4706127596905dd7bf261c02
1) fixed bug in type_introduction: first stage uses different namespace than second stage
2) fixed bug in dump_import_thy via gen2replay function

diff -r 6527ba893bae -r 7725da65f8e0 src/HOL/Import/hol4rews.ML
--- a/src/HOL/Import/hol4rews.ML	Fri Sep 23 18:47:47 2005 +0200
+++ b/src/HOL/Import/hol4rews.ML	Fri Sep 23 20:13:54 2005 +0200
@@ -558,6 +558,7 @@
     let
 	val output_dir = get_output_dir thy
 	val output_thy = get_output_thy thy
+	val input_thy = Context.theory_name thy
 	val import_segment = get_import_segment thy
 	val sg = sign_of thy
 	val os = TextIO.openOut (OS.Path.joinDirFile {dir=output_dir,
@@ -655,10 +656,20 @@
 		then ()
 		else out "\n\n"
 
+	fun gen2replay in_thy out_thy s = 
+	    let
+		val ss = NameSpace.unpack s
+	    in
+		if (hd ss = in_thy) then 
+		    NameSpace.pack (out_thy::(tl ss))
+		else
+		    s
+	    end 
+
 	val _ = if null mapped
 		then ()
 		else out "thm_maps"
-	val _ = app (fn (hol,isa) => out ("\n  " ^ (trans_string hol) ^ " > " ^ (trans_string isa))) mapped
+	val _ = app (fn (hol,isa) => out ("\n  " ^ (trans_string hol) ^ " > " ^ (trans_string (gen2replay input_thy output_thy isa)))) mapped
 	val _ = if null mapped 
 		then ()
 		else out "\n\n"
diff -r 6527ba893bae -r 7725da65f8e0 src/HOL/Import/proof_kernel.ML
--- a/src/HOL/Import/proof_kernel.ML	Fri Sep 23 18:47:47 2005 +0200
+++ b/src/HOL/Import/proof_kernel.ML	Fri Sep 23 20:13:54 2005 +0200
@@ -1177,7 +1177,7 @@
 
 fun get_isabelle_thm thyname thmname hol4conc thy =
     let
-	val _ = message "get_isabelle_thm called..."
+	val _ = writeln ("get_isabelle_thm called: "^thmname)
 	val sg = sign_of thy
 
 	val (info,hol4conc') = disamb_term hol4conc
@@ -1196,7 +1196,7 @@
 	case get_hol4_mapping thyname thmname thy of
 	    SOME (SOME thmname) =>
 	    let
-		val _ = message ("Looking for " ^ thmname)
+		val _ = writeln ("Looking for " ^ thmname)
 		val th1 = (SOME (transform_error (PureThy.get_thm thy) (Name thmname))
 			   handle ERROR_MESSAGE _ =>
 				  (case split_name thmname of
@@ -1213,14 +1213,14 @@
 	    end
 	  | SOME NONE => error ("Trying to access ignored theorem " ^ thmname)
 	  | NONE =>
-	    let
-		val _ = (message "Looking for conclusion:";
+	    let		
+		val _ = (writeln "Looking for conclusion:";
 			 if_debug prin isaconc)
 		val cs = non_trivial_term_consts isaconc
-		val _ = (message "Looking for consts:";
-			 message (commas cs))
+		val _ = (writeln "Looking for consts:";
+			 writeln (commas cs))
 		val pot_thms = Shuffler.find_potential thy isaconc
-		val _ = message ((Int.toString (length pot_thms)) ^ " potential theorems")
+		val _ = writeln ((Int.toString (length pot_thms)) ^ " potential theorems")
 	    in
 		case Shuffler.set_prop thy isaconc pot_thms of
 		    SOME (isaname,th) =>