changeset 59970 | e9f73d87d904 |
parent 59582 | 0fbed69ff081 |
child 69593 | 3dda49e08b9d |
--- a/src/HOL/Tools/ATP/atp_waldmeister.ML Wed Apr 08 16:24:22 2015 +0200 +++ b/src/HOL/Tools/ATP/atp_waldmeister.ML Wed Apr 08 19:39:08 2015 +0200 @@ -445,7 +445,7 @@ let val thy = Proof_Context.theory_of ctxt - val preproc = Object_Logic.atomize_term thy + val preproc = Object_Logic.atomize_term ctxt val conditions = map preproc hyps_t0 val consequence = preproc concl_t0