# HG changeset patch
# User wenzelm
# Date 1206740382 -3600
# Node ID f4c95646135324201557cc94bd2dc7a5064e2837
# Parent  e44d24620515c13d22230254f3a86d3c7651bc95
NAMED_CRITICAL;

diff -r e44d24620515 -r f4c956461353 src/Pure/pure_thy.ML
--- a/src/Pure/pure_thy.ML	Fri Mar 28 22:01:56 2008 +0100
+++ b/src/Pure/pure_thy.ML	Fri Mar 28 22:39:42 2008 +0100
@@ -220,7 +220,7 @@
 
 (* hiding -- affects current theory node only *)
 
-fun hide_thms fully names thy = CRITICAL (fn () =>
+fun hide_thms fully names thy = NAMED_CRITICAL "thm" (fn () =>
   let
     val r as ref (Thms {theorems = (space, thms), all_facts}) = get_theorems_ref thy;
     val space' = fold (NameSpace.hide fully) names space;
@@ -254,7 +254,7 @@
 
 (* add_thms_dynamic *)
 
-fun add_thms_dynamic (bname, f) thy = CRITICAL (fn () =>
+fun add_thms_dynamic (bname, f) thy = NAMED_CRITICAL "thm" (fn () =>
   let
     val name = Sign.full_name thy bname;
     val r as ref (Thms {theorems, all_facts}) = get_theorems_ref thy;
@@ -269,7 +269,7 @@
 fun warn_same name = warning ("Theorem database already contains a copy of " ^ quote name);
 
 fun enter_thms _ _ app_att ("", thms) thy = app_att (thy, thms) |> swap
-  | enter_thms pre_name post_name app_att (bname, thms) thy = CRITICAL (fn () =>
+  | enter_thms pre_name post_name app_att (bname, thms) thy = NAMED_CRITICAL "thm" (fn () =>
       let
         val name = Sign.full_name thy bname;
         val (thy', thms') = apsnd (post_name name) (app_att (thy, pre_name name thms));