src/HOL/Tools/SMT/smt_normalize.ML
changeset 59632 5980e75a204e
parent 59621 291934bac95e
child 60642 48dd1cefb4ae
     1.1 --- a/src/HOL/Tools/SMT/smt_normalize.ML	Fri Mar 06 23:44:51 2015 +0100
     1.2 +++ b/src/HOL/Tools/SMT/smt_normalize.ML	Fri Mar 06 23:44:57 2015 +0100
     1.3 @@ -31,7 +31,7 @@
     1.4  (** instantiate elimination rules **)
     1.5  
     1.6  local
     1.7 -  val (cpfalse, cfalse) = `SMT_Util.mk_cprop (Thm.global_cterm_of @{theory} @{const False})
     1.8 +  val (cpfalse, cfalse) = `SMT_Util.mk_cprop (Thm.cterm_of @{context} @{const False})
     1.9  
    1.10    fun inst f ct thm =
    1.11      let val cv = f (Drule.strip_imp_concl (Thm.cprop_of thm))
    1.12 @@ -189,7 +189,7 @@
    1.13    fun mk_pat ct = Thm.apply (SMT_Util.instT' ct pat) ct
    1.14  
    1.15    fun mk_clist T =
    1.16 -    apply2 (Thm.global_cterm_of @{theory}) (SMT_Util.symb_cons_const T, SMT_Util.symb_nil_const T)
    1.17 +    apply2 (Thm.cterm_of @{context}) (SMT_Util.symb_cons_const T, SMT_Util.symb_nil_const T)
    1.18    fun mk_list (ccons, cnil) f cts = fold_rev (Thm.mk_binop ccons o f) cts cnil
    1.19    val mk_pat_list = mk_list (mk_clist @{typ pattern})
    1.20    val mk_mpat_list = mk_list (mk_clist @{typ "pattern symb_list"})