src/Pure/thm.ML

   val cprem_of: thm -> int -> cterm
   val chyps_of: thm -> cterm list
   exception CONTEXT of string * ctyp list * cterm list * thm list * Context.generic option
   val theory_of_cterm: cterm -> theory
   val theory_of_thm: thm -> theory
+  val trim_context_ctyp: ctyp -> ctyp
   val trim_context_cterm: cterm -> cterm
   val trim_context: thm -> thm
   val transfer_cterm: theory -> cterm -> cterm
   val transfer: theory -> thm -> thm
   val transfer': Proof.context -> thm -> thm

   val combination: thm -> thm -> thm
   val equal_intr: thm -> thm -> thm
   val equal_elim: thm -> thm -> thm
   val flexflex_rule: Proof.context option -> thm -> thm Seq.seq
   val generalize: string list * string list -> int -> thm -> thm
+  val generalize_cterm: string list * string list -> int -> cterm -> cterm
+  val generalize_ctyp: string list -> int -> ctyp -> ctyp
   val instantiate: ((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list ->
     thm -> thm
   val instantiate_cterm: ((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list ->
     cterm -> cterm
   val trivial: cterm -> thm

 
 fun theory_of_thm th =
   Context.certificate_theory (cert_of th)
     handle ERROR msg => raise CONTEXT (msg, [], [], [th], NONE);
 
+fun trim_context_ctyp cT =
+  (case cT of
+    Ctyp {cert = Context.Certificate_Id _, ...} => cT
+  | Ctyp {cert = Context.Certificate thy, T, maxidx, sorts} =>
+      Ctyp {cert = Context.Certificate_Id (Context.theory_id thy),
+        T = T, maxidx = maxidx, sorts = sorts});
+
 fun trim_context_cterm ct =
   (case ct of
     Cterm {cert = Context.Certificate_Id _, ...} => ct
   | Cterm {cert = Context.Certificate thy, t, T, maxidx, sorts} =>
       Cterm {cert = Context.Certificate_Id (Context.theory_id thy),

           shyps = shyps,
           hyps = hyps,
           tpairs = tpairs',
           prop = prop'})
       end;
+
+fun generalize_cterm ([], []) _ ct = ct
+  | generalize_cterm (tfrees, frees) idx (ct as Cterm {cert, t, T, maxidx, sorts}) =
+      if idx <= maxidx then raise CTERM ("generalize_cterm: bad index", [ct])
+      else
+        Cterm {cert = cert, sorts = sorts,
+          T = Term_Subst.generalizeT tfrees idx T,
+          t = Term_Subst.generalize (tfrees, frees) idx t,
+          maxidx = Int.max (maxidx, idx)};
+
+fun generalize_ctyp [] _ cT = cT
+  | generalize_ctyp tfrees idx (Ctyp {cert, T, maxidx, sorts}) =
+      if idx <= maxidx then raise CTERM ("generalize_ctyp: bad index", [])
+      else
+        Ctyp {cert = cert, sorts = sorts,
+          T = Term_Subst.generalizeT tfrees idx T,
+          maxidx = Int.max (maxidx, idx)};
 
 
 (*Instantiation of schematic variables
            A
   --------------------