summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

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) =