src/HOL/Import/replay.ML

 	val _ = writeln ("Replaying (from cache) "^thmname^" ...")
 	fun rps [] thy = thy
 	  | rps (t::ts) thy = rps ts (rp t thy)
 	and rp (ThmEntry (thyname', thmname', aborted, History history)) thy = rps history thy	    
 	  | rp (DeltaEntry ds) thy = fold delta ds thy
-(*    datatype deltastate = Consts of (string * typ * mixfix) list
-			| Specification of (string * string * bool) list * term
-			| Hol_mapping of string * string * string
-			| Hol_pending of string * string * term
-			| Hol_const_mapping of string * string * string
-			| Hol_move of string * string
-			| Defs of string * term
-			| Hol_theorem of string * string * term
-			| 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
-*)
 	and delta (Specification (names, th)) thy = 
 	    fst (SpecificationPackage.add_specification NONE names (thy,th_of thy th))
 	  | delta (Hol_mapping (thyname, thmname, isaname)) thy = 
 	    add_hol4_mapping thyname thmname isaname thy
 	  | delta (Hol_pending (thyname, thmname, th)) thy = 

 	    fst(TypedefPackage.add_typedef_i false thmname typ c repabs (rtac (th_of thy th) 1) thy)
 	  | delta (Hol_type_mapping (thyname, tycname, fulltyname)) thy =  
 	    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)
+          | delta (Protect_varname (s,t)) thy = (P.replay_protect_varname s t; thy)
+	  | delta (Dump s) thy = P.replay_add_dump s thy
     in
 	rps
     end
 
 fun import_thms thyname int_thms thmnames thy =