--- a/src/HOL/Word/WordBitwise.thy Fri Mar 06 23:56:43 2015 +0100
+++ b/src/HOL/Word/WordBitwise.thy Fri Mar 06 23:57:01 2015 +0100
@@ -550,7 +550,6 @@
fun nat_get_Suc_simproc_fn n_sucs ctxt ct =
let
- val thy = Proof_Context.theory_of ctxt;
val (f $ arg) = Thm.term_of ct;
val n = (case arg of @{term nat} $ n => n | n => n)
|> HOLogic.dest_number |> snd;
@@ -560,7 +559,7 @@
(replicate i @{term Suc});
val _ = if arg = arg' then raise TERM ("", []) else ();
fun propfn g = HOLogic.mk_eq (g arg, g arg')
- |> HOLogic.mk_Trueprop |> Thm.global_cterm_of thy;
+ |> HOLogic.mk_Trueprop |> Thm.cterm_of ctxt;
val eq1 = Goal.prove_internal ctxt [] (propfn I)
(K (simp_tac (put_simpset word_ss ctxt) 1));
in Goal.prove_internal ctxt [] (propfn (curry (op $) f))