src/HOL/Tools/TFL/rules.ML

  *        Disjunction
  *---------------------------------------------------------------------------*)
 local val thy = Thm.theory_of_thm disjI1
       val prop = Thm.prop_of disjI1
       val [P,Q] = Misc_Legacy.term_vars prop
-      val disj1 = Thm.forall_intr (Thm.cterm_of thy Q) disjI1
+      val disj1 = Thm.forall_intr (Thm.global_cterm_of thy Q) disjI1
 in
 fun DISJ1 thm tm = thm RS (Thm.forall_elim (Dcterm.drop_prop tm) disj1)
   handle THM (msg, _, _) => raise RULES_ERR "DISJ1" msg;
 end;
 
 local val thy = Thm.theory_of_thm disjI2
       val prop = Thm.prop_of disjI2
       val [P,Q] = Misc_Legacy.term_vars prop
-      val disj2 = Thm.forall_intr (Thm.cterm_of thy P) disjI2
+      val disj2 = Thm.forall_intr (Thm.global_cterm_of thy P) disjI2
 in
 fun DISJ2 tm thm = thm RS (Thm.forall_elim (Dcterm.drop_prop tm) disj2)
   handle THM (msg, _, _) => raise RULES_ERR "DISJ2" msg;
 end;
 

  *---------------------------------------------------------------------------*)
 local (* this is fragile *)
       val thy = Thm.theory_of_thm spec
       val prop = Thm.prop_of spec
       val x = hd (tl (Misc_Legacy.term_vars prop))
-      val cTV = Thm.ctyp_of thy (type_of x)
-      val gspec = Thm.forall_intr (Thm.cterm_of thy x) spec
+      val cTV = Thm.global_ctyp_of thy (type_of x)
+      val gspec = Thm.forall_intr (Thm.global_cterm_of thy x) spec
 in
 fun SPEC tm thm =
    let val gspec' = Drule.instantiate_normalize ([(cTV, Thm.ctyp_of_cterm tm)], []) gspec
    in thm RS (Thm.forall_elim tm gspec') end
 end;

 
 (* Not optimized! Too complicated. *)
 local val thy = Thm.theory_of_thm allI
       val prop = Thm.prop_of allI
       val [P] = Misc_Legacy.add_term_vars (prop, [])
-      fun cty_theta s = map (fn (i, (S, ty)) => (Thm.ctyp_of s (TVar (i, S)), Thm.ctyp_of s ty))
+      fun cty_theta s = map (fn (i, (S, ty)) => (Thm.global_ctyp_of s (TVar (i, S)), Thm.global_ctyp_of s ty))
       fun ctm_theta s = map (fn (i, (_, tm2)) =>
-                             let val ctm2 = Thm.cterm_of s tm2
-                             in (Thm.cterm_of s (Var(i, Thm.typ_of_cterm ctm2)), ctm2)
+                             let val ctm2 = Thm.global_cterm_of s tm2
+                             in (Thm.global_cterm_of s (Var(i, Thm.typ_of_cterm ctm2)), ctm2)
                              end)
       fun certify s (ty_theta,tm_theta) =
         (cty_theta s (Vartab.dest ty_theta),
          ctm_theta s (Vartab.dest tm_theta))
 in

        val theta = Pattern.match thy (P,P') (Vartab.empty, Vartab.empty);
        val allI2 = Drule.instantiate_normalize (certify thy theta) allI
        val thm = Thm.implies_elim allI2 gth
        val tp $ (A $ Abs(_,_,M)) = Thm.prop_of thm
        val prop' = tp $ (A $ Abs(x,ty,M))
-   in ALPHA thm (Thm.cterm_of thy prop')
+   in ALPHA thm (Thm.global_cterm_of thy prop')
    end
 end;
 
 val GENL = fold_rev GEN;
 
 fun GEN_ALL thm =
    let val thy = Thm.theory_of_thm thm
        val prop = Thm.prop_of thm
-       val tycheck = Thm.cterm_of thy
+       val tycheck = Thm.global_cterm_of thy
        val vlist = map tycheck (Misc_Legacy.add_term_vars (prop, []))
   in GENL vlist thm
   end;
 
 

   let
     val lam = #2 (Dcterm.dest_comb (Dcterm.drop_prop (cconcl exth)))
     val redex = Dcterm.capply lam fvar
     val thy = Thm.theory_of_cterm redex
     val t$u = Thm.term_of redex
-    val residue = Thm.cterm_of thy (Term.betapply (t, u))
+    val residue = Thm.global_cterm_of thy (Term.betapply (t, u))
   in
     GEN fvar (DISCH residue fact) RS (exth RS Thms.choose_thm)
       handle THM (msg, _, _) => raise RULES_ERR "CHOOSE" msg
   end;
 

       val [P,x] = Misc_Legacy.term_vars prop
 in
 fun EXISTS (template,witness) thm =
    let val thy = Thm.theory_of_thm thm
        val prop = Thm.prop_of thm
-       val P' = Thm.cterm_of thy P
-       val x' = Thm.cterm_of thy x
+       val P' = Thm.global_cterm_of thy P
+       val x' = Thm.global_cterm_of thy x
        val abstr = #2 (Dcterm.dest_comb template)
    in
    thm RS (cterm_instantiate[(P',abstr), (x',witness)] exI)
      handle THM (msg, _, _) => raise RULES_ERR "EXISTS" msg
    end

  *---------------------------------------------------------------------------*)
 (* Could be improved, but needs "subst_free" for certified terms *)
 
 fun IT_EXISTS blist th =
    let val thy = Thm.theory_of_thm th
-       val tych = Thm.cterm_of thy
+       val tych = Thm.global_cterm_of thy
        val blist' = map (apply2 Thm.term_of) blist
-       fun ex v M  = Thm.cterm_of thy (USyntax.mk_exists{Bvar=v,Body = M})
+       fun ex v M  = Thm.global_cterm_of thy (USyntax.mk_exists{Bvar=v,Body = M})
 
   in
   fold_rev (fn (b as (r1,r2)) => fn thm =>
         EXISTS(ex r2 (subst_free [b]
                    (HOLogic.dest_Trueprop(Thm.prop_of thm))), tych r1)

               | Utils.ERR _ => get (rst, n+1, L);
 
 (* Note: Thm.rename_params_rule counts from 1, not 0 *)
 fun rename thm =
   let val thy = Thm.theory_of_thm thm
-      val tych = Thm.cterm_of thy
+      val tych = Thm.global_cterm_of thy
       val ants = Logic.strip_imp_prems (Thm.prop_of thm)
       val news = get (ants,1,[])
   in
   fold Thm.rename_params_rule news thm
   end;

              val dummy = print_thms ctxt "cntxt:" cntxt
              val dummy = say "cong rule:"
              val dummy = say (Display.string_of_thm ctxt thm)
              (* Unquantified eliminate *)
              fun uq_eliminate (thm,imp,thy) =
-                 let val tych = Thm.cterm_of thy
+                 let val tych = Thm.global_cterm_of thy
                      val dummy = print_cterm ctxt "To eliminate:" (tych imp)
                      val ants = map tych (Logic.strip_imp_prems imp)
                      val eq = Logic.strip_imp_concl imp
                      val lhs = tych(get_lhs eq)
                      val ctxt' = Simplifier.add_prems (map ASSUME ants) ctxt

               let val ((vstrl, _, used'), args) = dest_pbeta_redex used lhs_eq (length vlist)
                   val dummy = forall (op aconv) (ListPair.zip (vlist, args))
                     orelse error "assertion failed in CONTEXT_REWRITE_RULE"
                   val imp_body1 = subst_free (ListPair.zip (args, vstrl))
                                              imp_body
-                  val tych = Thm.cterm_of thy
+                  val tych = Thm.global_cterm_of thy
                   val ants1 = map tych (Logic.strip_imp_prems imp_body1)
                   val eq1 = Logic.strip_imp_concl imp_body1
                   val Q = get_lhs eq1
                   val QeqQ1 = pbeta_reduce (tych Q)
                   val Q1 = #2(Dcterm.dest_eq(cconcl QeqQ1))

               let val (vlist, imp_body, used') = strip_all used imp
                   val (ants,Q) = dest_impl imp_body
               in if (pbeta_redex Q) (length vlist)
                  then pq_eliminate (thm,thy,vlist,imp_body,Q)
                  else
-                 let val tych = Thm.cterm_of thy
+                 let val tych = Thm.global_cterm_of thy
                      val ants1 = map tych ants
                      val ctxt' = Simplifier.add_prems (map ASSUME ants1) ctxt
                      val Q_eeq_Q1 = Raw_Simplifier.rewrite_cterm
                         (false,true,false) (prover used') ctxt' (tych Q)
                       handle Utils.ERR _ => Thm.reflexive (tych Q)

               val rcontext = rev cntxt
               val cncl = HOLogic.dest_Trueprop o Thm.prop_of
               val antl = case rcontext of [] => []
                          | _   => [USyntax.list_mk_conj(map cncl rcontext)]
               val TC = genl(USyntax.list_mk_imp(antl, A))
-              val dummy = print_cterm ctxt "func:" (Thm.cterm_of thy func)
-              val dummy = print_cterm ctxt "TC:" (Thm.cterm_of thy (HOLogic.mk_Trueprop TC))
+              val dummy = print_cterm ctxt "func:" (Thm.global_cterm_of thy func)
+              val dummy = print_cterm ctxt "TC:" (Thm.global_cterm_of thy (HOLogic.mk_Trueprop TC))
               val dummy = tc_list := (TC :: !tc_list)
               val nestedp = is_some (USyntax.find_term is_func TC)
               val dummy = if nestedp then say "nested" else say "not_nested"
               val th' = if nestedp then raise RULES_ERR "solver" "nested function"
-                        else let val cTC = Thm.cterm_of thy
+                        else let val cTC = Thm.global_cterm_of thy
                                               (HOLogic.mk_Trueprop TC)
                              in case rcontext of
                                 [] => SPEC_ALL(ASSUME cTC)
                                | _ => MP (SPEC_ALL (ASSUME cTC))
                                          (LIST_CONJ rcontext)