diff -r 01265301db7f -r dd0c569fa43d TFL/post.ML
--- 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 =