src/HOL/Tools/Quotient/quotient_tacs.ML

     SOME (t, _) => t
   | _ => error "Solve_quotient_assm failed. Possibly a quotient theorem is missing."
 
 
 fun prep_trm thy (x, (T, t)) =
-  (Thm.cterm_of thy (Var (x, T)), Thm.cterm_of thy t)
+  (Thm.global_cterm_of thy (Var (x, T)), Thm.global_cterm_of thy t)
 
 fun prep_ty thy (x, (S, ty)) =
-  (Thm.ctyp_of thy (TVar (x, S)), Thm.ctyp_of thy ty)
+  (Thm.global_ctyp_of thy (TVar (x, S)), Thm.global_ctyp_of thy ty)
 
 fun get_match_inst thy pat trm =
   let
     val univ = Unify.matchers (Context.Theory thy) [(pat, trm)]
     val SOME (env, _) = Seq.pull univ           (* raises Bind, if no unifier *) (* FIXME fragile *)

 *)
 fun calculate_inst ctxt ball_bex_thm redex R1 R2 =
   let
     val thy = Proof_Context.theory_of ctxt
     fun get_lhs thm = fst (Logic.dest_equals (Thm.concl_of thm))
-    val ty_inst = map (SOME o Thm.ctyp_of thy) [domain_type (fastype_of R2)]
-    val trm_inst = map (SOME o Thm.cterm_of thy) [R2, R1]
+    val ty_inst = map (SOME o Thm.global_ctyp_of thy) [domain_type (fastype_of R2)]
+    val trm_inst = map (SOME o Thm.global_cterm_of thy) [R2, R1]
   in
     (case try (Drule.instantiate' ty_inst trm_inst) ball_bex_thm of
       NONE => NONE
     | SOME thm' =>
         (case try (get_match_inst thy (get_lhs thm')) redex of

   (case Thm.term_of ctrm of
     (Const (@{const_name Quot_True}, _) $ x) =>
       let
         val fx = fnctn x;
         val thy = Proof_Context.theory_of ctxt;
-        val cx = Thm.cterm_of thy x;
-        val cfx = Thm.cterm_of thy fx;
-        val cxt = Thm.ctyp_of thy (fastype_of x);
-        val cfxt = Thm.ctyp_of thy (fastype_of fx);
+        val cx = Thm.global_cterm_of thy x;
+        val cfx = Thm.global_cterm_of thy fx;
+        val cxt = Thm.global_ctyp_of thy (fastype_of x);
+        val cfxt = Thm.global_ctyp_of thy (fastype_of fx);
         val thm = Drule.instantiate' [SOME cxt, SOME cfxt] [SOME cx, SOME cfx] @{thm QT_imp}
       in
         Conv.rewr_conv thm ctrm
       end)
 

             let
               val ty_x = fastype_of x
               val ty_b = fastype_of qt_arg
               val ty_f = range_type (fastype_of f)
               val thy = Proof_Context.theory_of context
-              val ty_inst = map (SOME o Thm.ctyp_of thy) [ty_x, ty_b, ty_f]
-              val t_inst = map (SOME o Thm.cterm_of thy) [R2, f, g, x, y];
+              val ty_inst = map (SOME o Thm.global_ctyp_of thy) [ty_x, ty_b, ty_f]
+              val t_inst = map (SOME o Thm.global_cterm_of thy) [R2, f, g, x, y];
               val inst_thm = Drule.instantiate' ty_inst
                 ([NONE, NONE, NONE] @ t_inst) @{thm apply_rspQ3}
             in
               (rtac inst_thm THEN' SOLVED' (quotient_tac context)) 1
             end

 *)
 fun equals_rsp_tac R ctxt =
   let
     val thy = Proof_Context.theory_of ctxt
   in
-    case try (Thm.cterm_of thy) R of (* There can be loose bounds in R *)
+    case try (Thm.global_cterm_of thy) R of (* There can be loose bounds in R *)
       SOME ctm =>
         let
           val ty = domain_type (fastype_of R)
         in
-          case try (Drule.instantiate' [SOME (Thm.ctyp_of thy ty)]
-              [SOME (Thm.cterm_of thy R)]) @{thm equals_rsp} of
+          case try (Drule.instantiate' [SOME (Thm.global_ctyp_of thy ty)]
+              [SOME (Thm.global_cterm_of thy R)]) @{thm equals_rsp} of
             SOME thm => rtac thm THEN' quotient_tac ctxt
           | NONE => K no_tac
         end
     | _ => K no_tac
   end

     (case try bare_concl goal of
       SOME (rel $ _ $ (rep $ (abs $ _))) =>
         (let
           val thy = Proof_Context.theory_of ctxt;
           val (ty_a, ty_b) = dest_funT (fastype_of abs);
-          val ty_inst = map (SOME o Thm.ctyp_of thy) [ty_a, ty_b];
+          val ty_inst = map (SOME o Thm.global_ctyp_of thy) [ty_a, ty_b];
         in
-          case try (map (SOME o Thm.cterm_of thy)) [rel, abs, rep] of
+          case try (map (SOME o Thm.global_cterm_of thy)) [rel, abs, rep] of
             SOME t_inst =>
               (case try (Drule.instantiate' ty_inst t_inst) @{thm rep_abs_rsp} of
                 SOME inst_thm => (rtac inst_thm THEN' quotient_tac ctxt) i
               | NONE => no_tac)
           | NONE => no_tac

     (Const (@{const_name map_fun}, _) $ r1 $ a2) $ (Abs _) =>
       let
         val thy = Proof_Context.theory_of ctxt
         val (ty_b, ty_a) = dest_funT (fastype_of r1)
         val (ty_c, ty_d) = dest_funT (fastype_of a2)
-        val tyinst = map (SOME o Thm.ctyp_of thy) [ty_a, ty_b, ty_c, ty_d]
-        val tinst = [NONE, NONE, SOME (Thm.cterm_of thy r1), NONE, SOME (Thm.cterm_of thy a2)]
+        val tyinst = map (SOME o Thm.global_ctyp_of thy) [ty_a, ty_b, ty_c, ty_d]
+        val tinst = [NONE, NONE, SOME (Thm.global_cterm_of thy r1), NONE, SOME (Thm.global_cterm_of thy a2)]
         val thm1 = Drule.instantiate' tyinst tinst @{thm lambda_prs[THEN eq_reflection]}
         val thm2 = solve_quotient_assm ctxt (solve_quotient_assm ctxt thm1)
         val thm3 = rewrite_rule ctxt @{thms id_apply[THEN eq_reflection]} thm2
         val (insp, inst) =
           if ty_c = ty_d
           then make_inst_id (Thm.term_of (Thm.lhs_of thm3)) (Thm.term_of ctrm)
           else make_inst (Thm.term_of (Thm.lhs_of thm3)) (Thm.term_of ctrm)
         val thm4 =
-          Drule.instantiate_normalize ([], [(Thm.cterm_of thy insp, Thm.cterm_of thy inst)]) thm3
+          Drule.instantiate_normalize ([], [(Thm.global_cterm_of thy insp, Thm.global_cterm_of thy inst)]) thm3
       in
         Conv.rewr_conv thm4 ctrm
       end
   | _ => Conv.all_conv ctrm)
 

 fun gen_frees_tac ctxt =
   SUBGOAL (fn (concl, i) =>
     let
       val thy = Proof_Context.theory_of ctxt
       val vrs = Term.add_frees concl []
-      val cvrs = map (Thm.cterm_of thy o Free) vrs
+      val cvrs = map (Thm.global_cterm_of thy o Free) vrs
       val concl' = apply_under_Trueprop (all_list vrs) concl
       val goal = Logic.mk_implies (concl', concl)
       val rule = Goal.prove ctxt [] [] goal
         (K (EVERY1 [inst_spec_tac (rev cvrs), assume_tac ctxt]))
     in

       handle Quotient_Term.LIFT_MATCH msg => lift_match_error ctxt msg rtrm qtrm
     val inj_goal = Quotient_Term.inj_repabs_trm_chk ctxt (reg_goal, qtrm')
       handle Quotient_Term.LIFT_MATCH msg => lift_match_error ctxt msg rtrm qtrm
   in
     Drule.instantiate' []
-      [SOME (Thm.cterm_of thy rtrm'),
-       SOME (Thm.cterm_of thy reg_goal),
+      [SOME (Thm.global_cterm_of thy rtrm'),
+       SOME (Thm.global_cterm_of thy reg_goal),
        NONE,
-       SOME (Thm.cterm_of thy inj_goal)] procedure_thm
+       SOME (Thm.global_cterm_of thy inj_goal)] procedure_thm
   end
 
 
 (* Since we use Ball and Bex during the lifting and descending,
    we cannot deal with lemmas containing them, unless we unfold

       handle Quotient_Term.LIFT_MATCH msg => lift_match_error ctxt msg rtrm qtrm
     val inj_goal = Quotient_Term.inj_repabs_trm_chk ctxt (reg_goal, qtrm')
       handle Quotient_Term.LIFT_MATCH msg => lift_match_error ctxt msg rtrm qtrm
   in
     Drule.instantiate' []
-      [SOME (Thm.cterm_of thy reg_goal),
+      [SOME (Thm.global_cterm_of thy reg_goal),
        NONE,
-       SOME (Thm.cterm_of thy inj_goal)] partiality_procedure_thm
+       SOME (Thm.global_cterm_of thy inj_goal)] partiality_procedure_thm
   end
 
 
 fun partiality_descend_procedure_tac ctxt simps =
   let