structure Cla as defined in FOL;

--- a/src/ZF/Tools/datatype_package.ML	Tue Apr 26 22:18:07 2011 +0200
+++ b/src/ZF/Tools/datatype_package.ML	Tue Apr 26 22:22:39 2011 +0200
@@ -382,7 +382,7 @@
   (thy1 |> Sign.add_path big_rec_base_name
         |> Global_Theory.add_thmss
          [((Binding.name "simps", simps), [Simplifier.simp_add]),
-          ((Binding.empty , intrs), [Classical.safe_intro NONE]),
+          ((Binding.empty, intrs), [Cla.safe_intro NONE]),
           ((Binding.name "con_defs", con_defs), []),
           ((Binding.name "case_eqns", case_eqns), []),
           ((Binding.name "recursor_eqns", recursor_eqns), []),