# HG changeset patch
# User wenzelm
# Date 1198004073 -3600
# Node ID 891fe6b71d3b9c81f3f0af5eb7c9292a5b6f05f7
# Parent  8c335b4641a50081f4b35f4d8c69672ee95950a6
named some critical sections;

diff -r 8c335b4641a5 -r 891fe6b71d3b src/Pure/Isar/method.ML
--- a/src/Pure/Isar/method.ML	Tue Dec 18 19:54:32 2007 +0100
+++ b/src/Pure/Isar/method.ML	Tue Dec 18 19:54:33 2007 +0100
@@ -351,7 +351,7 @@
 val tactic_ref = ref ((fn _ => raise Match): Proof.context -> thm list -> tactic);
 fun set_tactic f = tactic_ref := f;
 
-fun ml_tactic txt ctxt = CRITICAL (fn () =>
+fun ml_tactic txt ctxt = NAMED_CRITICAL "ML" (fn () =>
   (ML_Context.use_mltext
     ("let fun tactic (ctxt: Proof.context) (facts: thm list) : tactic =\n"
       ^ txt ^ "\nin Method.set_tactic tactic end") false (SOME (Context.Proof ctxt));
diff -r 8c335b4641a5 -r 891fe6b71d3b src/Pure/Thy/thm_database.ML
--- a/src/Pure/Thy/thm_database.ML	Tue Dec 18 19:54:32 2007 +0100
+++ b/src/Pure/Thy/thm_database.ML	Tue Dec 18 19:54:33 2007 +0100
@@ -51,14 +51,14 @@
 fun ml_store_thm (name, thm) =
   let val thm' = store_thm (name, thm) in
     if warn_ml name then ()
-    else CRITICAL (fn () => (qed_thms := [thm'];
+    else NAMED_CRITICAL "ML" (fn () => (qed_thms := [thm'];
       use_text_verbose ("val " ^ name ^ " = hd (! ThmDatabase.qed_thms);")))
   end;
 
 fun ml_store_thms (name, thms) =
   let val thms' = store_thms (name, thms) in
     if warn_ml name then ()
-    else CRITICAL (fn () => (qed_thms := thms';
+    else NAMED_CRITICAL "ML" (fn () => (qed_thms := thms';
       use_text_verbose ("val " ^ name ^ " = ! ThmDatabase.qed_thms;")))
   end;