src/HOL/Tools/cnf.ML
changeset 59642 929984c529d3
parent 59621 291934bac95e
child 60696 8304fb4fb823
     1.1 --- a/src/HOL/Tools/cnf.ML	Fri Mar 06 23:55:55 2015 +0100
     1.2 +++ b/src/HOL/Tools/cnf.ML	Fri Mar 06 23:56:43 2015 +0100
     1.3 @@ -259,14 +259,13 @@
     1.4  
     1.5  fun make_under_quantifiers ctxt make t =
     1.6    let
     1.7 -    val thy = Proof_Context.theory_of ctxt
     1.8      fun conv ctxt ct =
     1.9        (case Thm.term_of ct of
    1.10          Const _ $ Abs _ => Conv.comb_conv (conv ctxt) ct
    1.11        | Abs _ => Conv.abs_conv (conv o snd) ctxt ct
    1.12        | Const _ => Conv.all_conv ct
    1.13        | t => make t RS eq_reflection)
    1.14 -  in conv ctxt (Thm.global_cterm_of thy t) RS meta_eq_to_obj_eq end
    1.15 +  in conv ctxt (Thm.cterm_of ctxt t) RS meta_eq_to_obj_eq end
    1.16  
    1.17  fun make_nnf_thm_under_quantifiers ctxt =
    1.18    make_under_quantifiers ctxt (make_nnf_thm (Proof_Context.theory_of ctxt))