# HG changeset patch
# User obua
# Date 1140059839 -3600
# Node ID c0321d7d6b3dafdf93bb2b716c156514a12ba7c4
# Parent  df24f2564aaa065dfc785c649c0626eb8f3b2a5d
variable counter is now also cached

diff -r df24f2564aaa -r c0321d7d6b3d src/HOL/Import/importrecorder.ML
--- a/src/HOL/Import/importrecorder.ML	Thu Feb 16 03:23:57 2006 +0100
+++ b/src/HOL/Import/importrecorder.ML	Thu Feb 16 04:17:19 2006 +0100
@@ -12,6 +12,7 @@
 			| Typedef of string option * (string * string list * mixfix) * term * (string * string) option * term 
 			| Hol_type_mapping of string * string * string
 			| Indexed_theorem of int * term
+	                | Protect_varname of string * string
 
     datatype history = History of history_entry list
 	 and history_entry = ThmEntry of string*string*bool*history | DeltaEntry of deltastate list
@@ -35,6 +36,7 @@
     val add_typedef :  string option -> string * string list * mixfix -> term -> (string * string) option -> thm -> unit
     val add_hol_type_mapping : string -> string -> string -> unit
     val add_indexed_theorem : int -> thm -> unit
+    val protect_varname : string -> string -> unit
 
     val set_skip_import_dir : string option -> unit
     val get_skip_import_dir : unit -> string option
@@ -60,6 +62,7 @@
 		    | Typedef of string option * (string * string list * mixfix) * term * (string * string) option * term 
 		    | Hol_type_mapping of string * string * string
 		    | Indexed_theorem of int * term
+	            | Protect_varname of string * string
 
 datatype history_entry = StartReplay of string*string  
 		       | StopReplay of string*string
@@ -104,6 +107,7 @@
       | delta (Typedef args) = wrap "typedef" typedef args
       | delta (Hol_type_mapping args) = wrap "hol_type_mapping" hol_type_mapping args
       | delta (Indexed_theorem args) = wrap "indexed_theorem" indexed_theorem args
+      | delta (Protect_varname args) = wrap "protect_varname" entry args
 
     fun history_entry (StartReplay args) = wrap "startreplay" entry args
       | history_entry (StopReplay args) = wrap "stopreplay" entry args
@@ -141,6 +145,7 @@
       | delta "typedef" = unwrap Typedef typedef
       | delta "hol_type_mapping" = unwrap Hol_type_mapping hol_type_mapping
       | delta "indexed_theorem" = unwrap Indexed_theorem indexed_theorem
+      | delta "protect_varname" = unwrap Protect_varname entry
       | delta _ = raise ParseException "delta"
 
     val delta = fn e => delta (name_of_wrap e) e
@@ -172,6 +177,7 @@
 fun add_hol_pending thyname thmname th = add_delta (Hol_pending (thyname, thmname, prop_of th))
 fun add_specification names th = add_delta (Specification (names, prop_of th)) 
 fun add_indexed_theorem i th = add_delta (Indexed_theorem (i, prop_of th))
+fun protect_varname s t = add_delta (Protect_varname (s,t))
 			    
 fun set_skip_import_dir dir = (history_dir := dir)
 fun get_skip_import_dir () = !history_dir
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))
diff -r df24f2564aaa -r c0321d7d6b3d src/HOL/Import/replay.ML
--- a/src/HOL/Import/replay.ML	Thu Feb 16 03:23:57 2006 +0100
+++ b/src/HOL/Import/replay.ML	Thu Feb 16 04:17:19 2006 +0100
@@ -361,6 +361,8 @@
 	    add_hol4_type_mapping thyname tycname true fulltyname thy
 	  | delta (Indexed_theorem (i, th)) thy = 
 	    (Array.update (int_thms,i-1,SOME (P.to_hol_thm (th_of thy th))); thy)	    	    
+          | delta (Protect_varname (s,t)) thy =
+	    (P.replay_protect_varname s t; thy)
     in
 	rps
     end