src/HOL/Decision_Procs/approximation_generator.ML
changeset 59629 0d77c51b5040
parent 59621 291934bac95e
child 59850 f339ff48a6ee
     1.1 --- a/src/HOL/Decision_Procs/approximation_generator.ML	Fri Mar 06 23:14:41 2015 +0100
     1.2 +++ b/src/HOL/Decision_Procs/approximation_generator.ML	Fri Mar 06 23:33:25 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.global_cterm_of thy r |> conv |> Thm.prop_of |> Logic.dest_equals |> snd
     1.8 +fun conv_term ctxt conv r = Thm.cterm_of ctxt 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
    1.12 @@ -138,7 +138,7 @@
    1.13            (AList.lookup op = (map dest_Free xs ~~ ts)
    1.14              #> the_default Term.dummy
    1.15              #> curry op $ @{term "real::float\<Rightarrow>_"}
    1.16 -            #> conv_term (Proof_Context.theory_of ctxt) (rewrite_with ctxt postproc_form_eqs))
    1.17 +            #> conv_term ctxt (rewrite_with ctxt postproc_form_eqs))
    1.18            frees
    1.19        in
    1.20          if approximate ctxt (mk_approx_form e ts) |> is_True
    1.21 @@ -159,13 +159,12 @@
    1.22      "\<not> (p \<and> q) \<longleftrightarrow> \<not> p \<or> \<not> q"
    1.23      "\<not> (p \<or> q) \<longleftrightarrow> \<not> p \<and> \<not> q"
    1.24      "\<not> \<not> q \<longleftrightarrow> q"
    1.25 -    by auto
    1.26 -  }
    1.27 +    by auto}
    1.28  
    1.29  fun reify_goal ctxt t =
    1.30    HOLogic.mk_not t
    1.31 -    |> conv_term (Proof_Context.theory_of ctxt) (rewrite_with ctxt preproc_form_eqs)
    1.32 -    |> conv_term (Proof_Context.theory_of ctxt) (Reification.conv ctxt form_equations)
    1.33 +    |> conv_term ctxt (rewrite_with ctxt preproc_form_eqs)
    1.34 +    |> conv_term ctxt (Reification.conv ctxt form_equations)
    1.35      |> dest_interpret_form
    1.36      ||> HOLogic.dest_list
    1.37