changeset 4397 | 7f760385a3a5 |
parent 4315 | f4bc2f6ee5e0 |
child 4439 | 02730662e446 |
--- a/src/Pure/thm.ML Fri Dec 12 17:11:26 1997 +0100 +++ b/src/Pure/thm.ML Fri Dec 12 17:14:58 1997 +0100 @@ -1833,7 +1833,7 @@ case proc signt prems eta_t of None => (trace false "FAILED"; proc_rews eta_t ps) | Some raw_thm => - (trace_thm false ("Procedure " ^ quote name ^ " proved rewrite rule:") raw_thm; + (trace_thm false ("Procedure " ^ quote name ^ " produced rewrite rule:") raw_thm; (case rews (mk_procrule raw_thm) of None => (trace false "IGNORED"; proc_rews eta_t ps) | some => some)))