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