1.1 --- a/src/HOL/Decision_Procs/approximation.ML Wed Sep 21 17:56:25 2016 +0200
1.2 +++ b/src/HOL/Decision_Procs/approximation.ML Tue Dec 06 17:21:34 2016 +0100
1.3 @@ -43,7 +43,7 @@
1.4 end
1.5
1.6 fun approximation_conv ctxt ct =
1.7 - approximation_oracle (Proof_Context.theory_of ctxt, Thm.term_of ct |> tap (tracing o Syntax.string_of_term ctxt));
1.8 + approximation_oracle (Proof_Context.theory_of ctxt, Thm.term_of ct);
1.9
1.10 fun approximate ctxt t =
1.11 approximation_oracle (Proof_Context.theory_of ctxt, t)