# HG changeset patch
# User wenzelm
# Date 1519234624 -3600
# Node ID 58f951ce71c884a4560019c7743c521e34c40024
# Parent  3d8d4f6d1d6436bb82674d14f27573d4e4ff1396
more operations for ctyp, cterm;

diff -r 3d8d4f6d1d64 -r 58f951ce71c8 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Wed Feb 21 16:26:42 2018 +0100
+++ b/src/Pure/thm.ML	Wed Feb 21 18:37:04 2018 +0100
@@ -75,6 +75,7 @@
   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
@@ -118,6 +119,8 @@
   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 ->
@@ -410,6 +413,13 @@
   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
@@ -1152,6 +1162,23 @@
           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