src/HOL/Tools/split_rule.ML

 
 (*Curries any Var of function type in the rule*)
 fun split_rule_var' (t as Var (v, Type ("fun", [T1, T2]))) rl =
       let val T' = HOLogic.flatten_tupleT T1 ---> T2;
           val newt = ap_split T1 T2 (Var (v, T'));
-          val cterm = Thm.cterm_of (Thm.theory_of_thm rl);
+          val cterm = Thm.global_cterm_of (Thm.theory_of_thm rl);
       in Thm.instantiate ([], [(cterm t, cterm newt)]) rl end
   | split_rule_var' _ rl = rl;
 
 
 (* complete splitting of partially split rules *)

         (incr_boundvars 1 u) $ Bound 0))
   | ap_split' _ _ u = u;
 
 fun complete_split_rule_var (t as Var (v, T), ts) (rl, vs) =
       let
-        val cterm = Thm.cterm_of (Thm.theory_of_thm rl)
+        val cterm = Thm.global_cterm_of (Thm.theory_of_thm rl)
         val (Us', U') = strip_type T;
         val Us = take (length ts) Us';
         val U = drop (length ts) Us' ---> U';
         val T' = maps HOLogic.flatten_tupleT Us ---> U;
         fun mk_tuple (v as Var ((a, _), T)) (xs, insts) =

               in (xs @ ys, (cterm v, cterm (HOLogic.mk_ptuple (HOLogic.flat_tupleT_paths T) T
                 (map (Var o apfst (rpair 0)) (ys ~~ Ts))))::insts)
               end
           | mk_tuple _ x = x;
         val newt = ap_split' Us U (Var (v, T'));
-        val cterm = Thm.cterm_of (Thm.theory_of_thm rl);
+        val cterm = Thm.global_cterm_of (Thm.theory_of_thm rl);
         val (vs', insts) = fold mk_tuple ts (vs, []);
       in
         (Drule.instantiate_normalize ([], [(cterm t, cterm newt)] @ insts) rl, vs')
       end
   | complete_split_rule_var _ x = x;