src/HOL/Decision_Procs/approximation_generator.ML
changeset 59621 291934bac95e
parent 59582 0fbed69ff081
child 59629 0d77c51b5040
     1.1 --- a/src/HOL/Decision_Procs/approximation_generator.ML	Fri Mar 06 14:01:08 2015 +0100
     1.2 +++ b/src/HOL/Decision_Procs/approximation_generator.ML	Fri Mar 06 15:58:56 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 = Thm.cterm_of thy r |> conv |> Thm.prop_of |> Logic.dest_equals |> snd
     1.8 +fun conv_term thy conv r = Thm.global_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