--- 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));