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