named some critical sections;
authorwenzelm
Tue Dec 18 19:54:33 2007 +0100 (2007-12-18)
changeset 25699891fe6b71d3b
parent 25698 8c335b4641a5
child 25700 185ea28035ac
named some critical sections;
src/Pure/Isar/method.ML
src/Pure/Thy/thm_database.ML
     1.1 --- a/src/Pure/Isar/method.ML	Tue Dec 18 19:54:32 2007 +0100
     1.2 +++ b/src/Pure/Isar/method.ML	Tue Dec 18 19:54:33 2007 +0100
     1.3 @@ -351,7 +351,7 @@
     1.4  val tactic_ref = ref ((fn _ => raise Match): Proof.context -> thm list -> tactic);
     1.5  fun set_tactic f = tactic_ref := f;
     1.6  
     1.7 -fun ml_tactic txt ctxt = CRITICAL (fn () =>
     1.8 +fun ml_tactic txt ctxt = NAMED_CRITICAL "ML" (fn () =>
     1.9    (ML_Context.use_mltext
    1.10      ("let fun tactic (ctxt: Proof.context) (facts: thm list) : tactic =\n"
    1.11        ^ txt ^ "\nin Method.set_tactic tactic end") false (SOME (Context.Proof ctxt));
     2.1 --- a/src/Pure/Thy/thm_database.ML	Tue Dec 18 19:54:32 2007 +0100
     2.2 +++ b/src/Pure/Thy/thm_database.ML	Tue Dec 18 19:54:33 2007 +0100
     2.3 @@ -51,14 +51,14 @@
     2.4  fun ml_store_thm (name, thm) =
     2.5    let val thm' = store_thm (name, thm) in
     2.6      if warn_ml name then ()
     2.7 -    else CRITICAL (fn () => (qed_thms := [thm'];
     2.8 +    else NAMED_CRITICAL "ML" (fn () => (qed_thms := [thm'];
     2.9        use_text_verbose ("val " ^ name ^ " = hd (! ThmDatabase.qed_thms);")))
    2.10    end;
    2.11  
    2.12  fun ml_store_thms (name, thms) =
    2.13    let val thms' = store_thms (name, thms) in
    2.14      if warn_ml name then ()
    2.15 -    else CRITICAL (fn () => (qed_thms := thms';
    2.16 +    else NAMED_CRITICAL "ML" (fn () => (qed_thms := thms';
    2.17        use_text_verbose ("val " ^ name ^ " = ! ThmDatabase.qed_thms;")))
    2.18    end;
    2.19