69 else (warning ("Cannot bind theorem(s) " ^ quote name ^ " as ML value"); true); |
69 else (warning ("Cannot bind theorem(s) " ^ quote name ^ " as ML value"); true); |
70 |
70 |
71 fun ml_store_thm (name, thm) = |
71 fun ml_store_thm (name, thm) = |
72 let val thm' = store_thm (name, thm) in |
72 let val thm' = store_thm (name, thm) in |
73 if warn_ml name then () |
73 if warn_ml name then () |
74 else (qed_thms := [thm]; use_text true ("val " ^ name ^ " = hd (! ThmDatabase.qed_thms);")) |
74 else (qed_thms := [thm']; use_text true ("val " ^ name ^ " = hd (! ThmDatabase.qed_thms);")) |
75 end; |
75 end; |
76 |
76 |
77 fun ml_store_thms (name, thms) = |
77 fun ml_store_thms (name, thms) = |
78 let val thms' = store_thms (name, thms) in |
78 let val thms' = store_thms (name, thms) in |
79 if warn_ml name then () |
79 if warn_ml name then () |
80 else (qed_thms := thms; use_text true ("val " ^ name ^ " = ! ThmDatabase.qed_thms;")) |
80 else (qed_thms := thms'; use_text true ("val " ^ name ^ " = ! ThmDatabase.qed_thms;")) |
81 end; |
81 end; |
82 |
82 |
83 fun bind_thm (name, thm) = ml_store_thm (name, standard thm); |
83 fun bind_thm (name, thm) = ml_store_thm (name, standard thm); |
84 fun bind_thms (name, thms) = ml_store_thms (name, map standard thms); |
84 fun bind_thms (name, thms) = ml_store_thms (name, map standard thms); |
85 |
85 |