src/Pure/Thy/thm_database.ML
changeset 25699 891fe6b71d3b
parent 23921 947152add153
child 26386 9c806de22a6a
     1.1 --- a/src/Pure/Thy/thm_database.ML	Tue Dec 18 19:54:32 2007 +0100
     1.2 +++ b/src/Pure/Thy/thm_database.ML	Tue Dec 18 19:54:33 2007 +0100
     1.3 @@ -51,14 +51,14 @@
     1.4  fun ml_store_thm (name, thm) =
     1.5    let val thm' = store_thm (name, thm) in
     1.6      if warn_ml name then ()
     1.7 -    else CRITICAL (fn () => (qed_thms := [thm'];
     1.8 +    else NAMED_CRITICAL "ML" (fn () => (qed_thms := [thm'];
     1.9        use_text_verbose ("val " ^ name ^ " = hd (! ThmDatabase.qed_thms);")))
    1.10    end;
    1.11  
    1.12  fun ml_store_thms (name, thms) =
    1.13    let val thms' = store_thms (name, thms) in
    1.14      if warn_ml name then ()
    1.15 -    else CRITICAL (fn () => (qed_thms := thms';
    1.16 +    else NAMED_CRITICAL "ML" (fn () => (qed_thms := thms';
    1.17        use_text_verbose ("val " ^ name ^ " = ! ThmDatabase.qed_thms;")))
    1.18    end;
    1.19