diff -r df24f2564aaa -r c0321d7d6b3d src/HOL/Import/proof_kernel.ML
--- a/src/HOL/Import/proof_kernel.ML	Thu Feb 16 03:23:57 2006 +0100
+++ b/src/HOL/Import/proof_kernel.ML	Thu Feb 16 04:17:19 2006 +0100
@@ -112,7 +112,8 @@
     val new_axiom : string -> term -> theory -> theory * thm
 
     val prin : term -> unit 
-    val protect_factname : string -> string
+    val protect_factname : string -> string 
+    val replay_protect_varname : string -> string -> unit
 end
 
 structure ProofKernel :> ProofKernel =
@@ -480,11 +481,26 @@
       let
 	  val _ = invented_isavar := IntInf.+ (!invented_isavar, IntInf.fromInt 1)
 	  val t = "u_"^(IntInf.toString (!invented_isavar))
+	  val _ = ImportRecorder.protect_varname s t
           val _ = protected_varnames := Symtab.update (s, t) (!protected_varnames)
       in
 	  t
       end
 
+exception REPLAY_PROTECT_VARNAME of string*string*string
+
+fun replay_protect_varname s t = 
+	case Symtab.lookup (!protected_varnames) s of
+	  SOME t' => raise REPLAY_PROTECT_VARNAME (s, t, t')
+	| NONE => 	
+          let
+	      val _ = invented_isavar := IntInf.+ (!invented_isavar, IntInf.fromInt 1)
+	      val t = "u_"^(IntInf.toString (!invented_isavar))
+              val _ = protected_varnames := Symtab.update (s, t) (!protected_varnames)
+          in
+	      ()
+          end	       	
+	 
 fun protect_boundvarname s = if innocent_varname s andalso valid_boundvarname s then s else "u"
 
 fun mk_lambda (v as Free (x, T)) t = Abs (protect_boundvarname x, T, abstract_over (v, t))