--- a/src/Pure/pure_thy.ML Mon Jul 23 16:45:00 2007 +0200
+++ b/src/Pure/pure_thy.ML Mon Jul 23 16:45:01 2007 +0200
@@ -304,11 +304,11 @@
(* hiding -- affects current theory node only *)
-fun hide_thms fully names thy =
+fun hide_thms fully names thy = CRITICAL (fn () =>
let
val r as ref {theorems = (space, thms), index} = get_theorems_ref thy;
val space' = fold (NameSpace.hide fully) names space;
- in r := {theorems = (space', thms), index = index}; thy end;
+ in r := {theorems = (space', thms), index = index}; thy end);
(* fact specifications *)
@@ -343,7 +343,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 =
+ | enter_thms pre_name post_name app_att (bname, thms) thy = CRITICAL (fn () =>
let
val name = Sign.full_name thy bname;
val (thy', thms') = apsnd (post_name name) (app_att (thy, pre_name name thms));
@@ -359,7 +359,7 @@
else warn_overwrite name);
r := {theorems = (space', theorems'), index = index'};
(thms', thy')
- end;
+ end);
(* add_thms(s) *)