--- a/src/ZF/Tools/ind_cases.ML Fri Feb 11 18:51:00 2005 +0100
+++ b/src/ZF/Tools/ind_cases.ML Sun Feb 13 17:15:14 2005 +0100
@@ -42,8 +42,8 @@
(Logic.strip_imp_concl A)))))) handle TERM _ => err ();
in
(case Symtab.lookup (IndCasesData.get thy, c) of
- None => error ("Unknown inductive cases rule for set " ^ quote c)
- | Some f => f ss (Thm.cterm_of (Theory.sign_of thy) A))
+ NONE => error ("Unknown inductive cases rule for set " ^ quote c)
+ | SOME f => f ss (Thm.cterm_of (Theory.sign_of thy) A))
end;