changeset 14836 | ba0fc27a6c7e |
parent 14643 | 130076a81b84 |
child 15011 | 35be762f58f9 |
--- a/TFL/rules.ML Sat May 29 15:06:42 2004 +0200 +++ b/TFL/rules.ML Sat May 29 15:07:05 2004 +0200 @@ -817,7 +817,7 @@ let val result = if strict then Goals.prove_goalw_cterm [] ptm (fn _ => [tac]) else - Library.transform_error (fn () => + transform_error (fn () => Goals.prove_goalw_cterm [] ptm (fn _ => [tac])) () handle ERROR_MESSAGE msg => (warning msg; raise RULES_ERR "prove" msg); in #1 (freeze_thaw result) end;