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)
```