1.1 --- a/src/HOL/Decision_Procs/Approximation.thy	Tue Oct 20 20:54:31 2009 +0200
     1.2 +++ b/src/HOL/Decision_Procs/Approximation.thy	Tue Oct 20 21:22:37 2009 +0200
     1.3 @@ -3462,9 +3462,9 @@
     1.4  
     1.5    fun approx_form prec ctxt t =
     1.6            realify t
     1.7 -       |> prepare_form (Context.theory_of_proof ctxt)
     1.8 +       |> prepare_form (ProofContext.theory_of ctxt)
     1.9         |> (fn arith_term =>
    1.10 -          reify_form (Context.theory_of_proof ctxt) arith_term
    1.11 +          reify_form (ProofContext.theory_of ctxt) arith_term
    1.12         |> HOLogic.dest_Trueprop |> dest_interpret_form
    1.13         |> (fn (data, xs) =>
    1.14            mk_approx_form_eval prec data (HOLogic.mk_list @{typ "(float * float) option"}