src/Pure/Thy/thm_database.ML
changeset 23921 947152add153
parent 22144 c33450acd873
child 25699 891fe6b71d3b
     1.1 --- a/src/Pure/Thy/thm_database.ML	Mon Jul 23 13:50:31 2007 +0200
     1.2 +++ b/src/Pure/Thy/thm_database.ML	Mon Jul 23 14:06:11 2007 +0200
     1.3 @@ -51,14 +51,15 @@
     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 (qed_thms := [thm'];
     1.8 -      use_text_verbose ("val " ^ name ^ " = hd (! ThmDatabase.qed_thms);"))
     1.9 +    else CRITICAL (fn () => (qed_thms := [thm'];
    1.10 +      use_text_verbose ("val " ^ name ^ " = hd (! ThmDatabase.qed_thms);")))
    1.11    end;
    1.12  
    1.13  fun ml_store_thms (name, thms) =
    1.14    let val thms' = store_thms (name, thms) in
    1.15      if warn_ml name then ()
    1.16 -    else (qed_thms := thms'; use_text_verbose ("val " ^ name ^ " = ! ThmDatabase.qed_thms;"))
    1.17 +    else CRITICAL (fn () => (qed_thms := thms';
    1.18 +      use_text_verbose ("val " ^ name ^ " = ! ThmDatabase.qed_thms;")))
    1.19    end;
    1.20  
    1.21