--- a/src/HOL/Import/replay.ML Tue Mar 07 14:09:48 2006 +0100
+++ b/src/HOL/Import/replay.ML Tue Mar 07 16:03:31 2006 +0100
@@ -369,7 +369,13 @@
(entry::cached, normal)
end)
else
- raise ERR "import_thms" ("cached theorems are not in-sync, expected: "^thmname^", found: "^thmname')
+ let
+ val _ = writeln ("cached theorems are not in-sync, expected: "^thmname^", found: "^thmname')
+ val _ = writeln ("proceeding with next uncached theorem...")
+ in
+ ([], thmname::names)
+ end
+ (* raise ERR "import_thms" ("cached theorems are not in-sync, expected: "^thmname^", found: "^thmname')*)
| zip (thmname::_) (DeltaEntry _ :: _) =
raise ERR "import_thms" ("expected theorem '"^thmname^"', but found a delta")
fun zip' xs (History ys) =