src/HOL/Import/replay.ML
changeset 19067 c0321d7d6b3d
parent 19064 bf19cc5a7899
child 19068 04b302f2902d
     1.1 --- a/src/HOL/Import/replay.ML	Thu Feb 16 03:23:57 2006 +0100
     1.2 +++ b/src/HOL/Import/replay.ML	Thu Feb 16 04:17:19 2006 +0100
     1.3 @@ -361,6 +361,8 @@
     1.4  	    add_hol4_type_mapping thyname tycname true fulltyname thy
     1.5  	  | delta (Indexed_theorem (i, th)) thy = 
     1.6  	    (Array.update (int_thms,i-1,SOME (P.to_hol_thm (th_of thy th))); thy)	    	    
     1.7 +          | delta (Protect_varname (s,t)) thy =
     1.8 +	    (P.replay_protect_varname s t; thy)
     1.9      in
    1.10  	rps
    1.11      end