summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

TFL/post.ML

changeset 18678 | dd0c569fa43d |

parent 18139 | b15981aedb7b |

child 19736 | d8d0f8f51d69 |

--- a/TFL/post.ML Fri Jan 13 17:39:41 2006 +0100 +++ b/TFL/post.ML Sat Jan 14 17:14:06 2006 +0100 @@ -207,7 +207,7 @@ List.mapPartial ((fn (r,x) => if x = i then SOME r else NONE)); fun solve_eq (th, [], i) = - raise ERROR_MESSAGE "derive_init_eqs: missing rules" + error "derive_init_eqs: missing rules" | solve_eq (th, [a], i) = [(a, i)] | solve_eq (th, splitths as (_ :: _), i) = (writeln "Proving unsplit equation..."; @@ -215,7 +215,7 @@ (CaseSplit.splitto splitths th), i)]) (* if there's an error, pretend nothing happened with this definition We should probably print something out so that the user knows...? *) - handle ERROR_MESSAGE s => + handle ERROR s => (warning ("recdef (solve_eq): " ^ s); map (fn x => (x,i)) splitths); in fun derive_init_eqs sgn rules eqs =