src/HOL/Tools/numeral_simprocs.ML
changeset 59621 291934bac95e
parent 59586 ddf6deaadfe8
child 59642 929984c529d3
     1.1 --- a/src/HOL/Tools/numeral_simprocs.ML	Fri Mar 06 14:01:08 2015 +0100
     1.2 +++ b/src/HOL/Tools/numeral_simprocs.ML	Fri Mar 06 15:58:56 2015 +0100
     1.3 @@ -483,7 +483,7 @@
     1.4      simplify_one ctxt (([th, cancel_th]) MRS trans);
     1.5  
     1.6  local
     1.7 -  val Tp_Eq = Thm.reflexive (Thm.cterm_of @{theory HOL} HOLogic.Trueprop)
     1.8 +  val Tp_Eq = Thm.reflexive (Thm.global_cterm_of @{theory HOL} HOLogic.Trueprop)
     1.9    fun Eq_True_elim Eq = 
    1.10      Thm.equal_elim (Thm.combination Tp_Eq (Thm.symmetric Eq)) @{thm TrueI}
    1.11  in
    1.12 @@ -494,7 +494,7 @@
    1.13        val pos = less $ zero $ t and neg = less $ t $ zero
    1.14        val thy = Proof_Context.theory_of ctxt
    1.15        fun prove p =
    1.16 -        SOME (Eq_True_elim (Simplifier.asm_rewrite ctxt (Thm.cterm_of thy p)))
    1.17 +        SOME (Eq_True_elim (Simplifier.asm_rewrite ctxt (Thm.global_cterm_of thy p)))
    1.18          handle THM _ => NONE
    1.19      in case prove pos of
    1.20           SOME th => SOME(th RS pos_th)