src/HOL/Import/replay.ML
changeset 19203 778507520684
parent 19068 04b302f2902d
child 19349 36e537f89585
     1.1 --- a/src/HOL/Import/replay.ML	Tue Mar 07 14:09:48 2006 +0100
     1.2 +++ b/src/HOL/Import/replay.ML	Tue Mar 07 16:03:31 2006 +0100
     1.3 @@ -369,7 +369,13 @@
     1.4  		     (entry::cached, normal)
     1.5  		 end)
     1.6  	    else
     1.7 -		raise ERR "import_thms" ("cached theorems are not in-sync, expected: "^thmname^", found: "^thmname')
     1.8 +		let
     1.9 +		    val _ = writeln ("cached theorems are not in-sync,  expected: "^thmname^", found: "^thmname')
    1.10 +		    val _ = writeln ("proceeding with next uncached theorem...")
    1.11 +		in
    1.12 +		    ([], thmname::names)
    1.13 +		end
    1.14 +	(*	raise ERR "import_thms" ("cached theorems are not in-sync, expected: "^thmname^", found: "^thmname')*)
    1.15  	  | zip (thmname::_) (DeltaEntry _ :: _) = 
    1.16   	    raise ERR "import_thms" ("expected theorem '"^thmname^"', but found a delta")
    1.17  	fun zip' xs (History ys) =