src/HOL/Decision_Procs/Cooper.thy

     | Abs p => term_bools acc (snd (Syntax_Trans.variant_abs p))  (* FIXME !? *)
     | _ => if is_ty t orelse is_op t then acc else insert (op aconv) t acc)
   end;
 
 in
-  fn ct =>
+  fn (ctxt, t) =>
     let
-      val thy = Thm.theory_of_cterm ct;
-      val t = Thm.term_of ct;
       val fs = Misc_Legacy.term_frees t;
       val bs = term_bools [] t;
       val vs = map_index swap fs;
       val ps = map_index swap bs;
-      val t' = (term_of_fm ps vs o @{code pa} o fm_of_term ps vs) t;
-    in Thm.global_cterm_of thy (HOLogic.mk_Trueprop (HOLogic.mk_eq (t, t'))) end
+      val t' = term_of_fm ps vs (@{code pa} (fm_of_term ps vs t));
+    in Thm.cterm_of ctxt (HOLogic.mk_Trueprop (HOLogic.mk_eq (t, t'))) end
 end;
 *}
 
 ML_file "cooper_tac.ML"