src/HOL/Decision_Procs/approximation_generator.ML
changeset 59582 0fbed69ff081
parent 58988 6ebf918128b9
child 59621 291934bac95e
     1.1 --- a/src/HOL/Decision_Procs/approximation_generator.ML	Tue Mar 03 19:08:04 2015 +0100
     1.2 +++ b/src/HOL/Decision_Procs/approximation_generator.ML	Wed Mar 04 19:53:18 2015 +0100
     1.3 @@ -117,7 +117,7 @@
     1.4    }
     1.5  
     1.6  fun rewrite_with ctxt thms = Simplifier.rewrite (put_simpset HOL_basic_ss ctxt addsimps thms)
     1.7 -fun conv_term thy conv r = cterm_of thy r |> conv |> Thm.prop_of |> Logic.dest_equals |> snd
     1.8 +fun conv_term thy conv r = Thm.cterm_of thy r |> conv |> Thm.prop_of |> Logic.dest_equals |> snd
     1.9  
    1.10  fun approx_random ctxt prec eps frees e xs genuine_only size seed =
    1.11    let