diff -r 34f72eb7d2db -r 219e543496a3 src/FOL/FOL.thy
--- a/src/FOL/FOL.thy	Fri Nov 09 10:26:16 2001 +0100
+++ b/src/FOL/FOL.thy	Fri Nov 09 22:50:32 2001 +0100
@@ -20,7 +20,7 @@
 subsection {* Lemmas and proof tools *}
 
 use "FOL_lemmas1.ML"
-theorems case_split = case_split_thm [case_names True False]
+theorems case_split = case_split_thm [case_names True False, cases type: o]
 
 use "cladata.ML"
 setup Cla.setup