# HG changeset patch
# User wenzelm
# Date 1303849359 -7200
# Node ID 54450fa0d78b880cf61765aedde13d9479915331
# Parent  f4f011d1bf0b36fa88b7887a1b8b0626fed5f3e6
structure Cla as defined in FOL;

diff -r f4f011d1bf0b -r 54450fa0d78b src/ZF/Tools/datatype_package.ML
--- 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), []),