--- a/src/HOL/Decision_Procs/approximation_generator.ML Tue Mar 03 19:08:04 2015 +0100
+++ b/src/HOL/Decision_Procs/approximation_generator.ML Wed Mar 04 19:53:18 2015 +0100
@@ -117,7 +117,7 @@
}
fun rewrite_with ctxt thms = Simplifier.rewrite (put_simpset HOL_basic_ss ctxt addsimps thms)
-fun conv_term thy conv r = cterm_of thy r |> conv |> Thm.prop_of |> Logic.dest_equals |> snd
+fun conv_term thy conv r = Thm.cterm_of thy r |> conv |> Thm.prop_of |> Logic.dest_equals |> snd
fun approx_random ctxt prec eps frees e xs genuine_only size seed =
let