# HG changeset patch
# User wenzelm
# Date 1007518206 -3600
# Node ID 59874c94d0aa721b2510a563eca2429eccc744fe
# Parent  704e50ab65af63e1c5e2ceb1d22d0260cfbc53c0
ContextRules.intro_bang_global;

diff -r 704e50ab65af -r 59874c94d0aa src/HOL/Tools/record_package.ML
--- a/src/HOL/Tools/record_package.ML	Wed Dec 05 03:09:21 2001 +0100
+++ b/src/HOL/Tools/record_package.ML	Wed Dec 05 03:10:06 2001 +0100
@@ -912,7 +912,7 @@
       thms_thy |> PureThy.add_thms
        [(("induct", induct0), induct_type_global name),
         (("cases", cases0), cases_type_global name),
-        (("equality", equality), [Classical.xtra_intro_global])]
+        (("equality", equality), [ContextRules.intro_bang_global None])]
       |>> (#1 oo PureThy.add_thmss)
         [(("more_induct", more_induct), induct_type_global ""),
          (("more_cases", more_cases), cases_type_global "")];