--- a/src/HOL/Tools/inductive_codegen.ML Wed Apr 06 18:13:30 2005 +0200
+++ b/src/HOL/Tools/inductive_codegen.ML Thu Apr 07 09:24:35 2005 +0200
@@ -229,7 +229,7 @@
term_vs t subset vs andalso
forall is_eqT dupTs
end)
- (modes_of modes t handle OPTION => [Mode (([], []), [])])
+ (modes_of modes t handle Option => [Mode (([], []), [])])
| Sidecond t => if term_vs t subset vs then SOME (Mode (([], []), []))
else NONE) ps);
@@ -590,7 +590,7 @@
end;
fun find_mode s u modes is = (case find_first (fn Mode ((_, js), _) => is=js)
- (modes_of modes u handle OPTION => []) of
+ (modes_of modes u handle Option => []) of
NONE => error ("No such mode for " ^ s ^ ": " ^ string_of_mode ([], is))
| mode => mode);