src/HOL/Word/WordBitwise.thy

       else (n, 0);
     val arg' = List.foldr (op $) (HOLogic.mk_number @{typ nat} j)
         (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.cterm_of thy;
+      |> HOLogic.mk_Trueprop |> Thm.global_cterm_of thy;
     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))
       (K (simp_tac (put_simpset HOL_ss ctxt addsimps [eq1]) 1))
        |> mk_meta_eq |> SOME end