# HG changeset patch
# User wenzelm
# Date 1555178308 -7200
# Node ID 5d8833499c4aa1a253e388646c671a904203100f
# Parent  169d167554bd442ad6005d6af907df6a2f66392d
more ctyp operations;

diff -r 169d167554bd -r 5d8833499c4a src/Pure/thm.ML
--- a/src/Pure/thm.ML	Sat Apr 13 19:27:12 2019 +0200
+++ b/src/Pure/thm.ML	Sat Apr 13 19:58:28 2019 +0200
@@ -26,6 +26,7 @@
   val ctyp_of: Proof.context -> typ -> ctyp
   val dest_ctyp: ctyp -> ctyp list
   val dest_ctyp_nth: int -> ctyp -> ctyp
+  val make_ctyp: ctyp -> ctyp list -> ctyp
   (*certified terms*)
   val term_of: cterm -> term
   val typ_of_cterm: cterm -> typ
@@ -81,6 +82,7 @@
   val trim_context_ctyp: ctyp -> ctyp
   val trim_context_cterm: cterm -> cterm
   val trim_context: thm -> thm
+  val transfer_ctyp: theory -> ctyp -> ctyp
   val transfer_cterm: theory -> cterm -> cterm
   val transfer: theory -> thm -> thm
   val transfer': Proof.context -> thm -> thm
@@ -184,6 +186,25 @@
     | _ => err ())
   end;
 
+fun join_certificate_ctyp (Ctyp {cert, ...}) cert0 = Context.join_certificate (cert0, cert);
+fun union_sorts_ctyp (Ctyp {sorts, ...}) sorts0 = Sorts.union sorts0 sorts;
+fun maxidx_ctyp (Ctyp {maxidx, ...}) maxidx0 = Int.max (maxidx0, maxidx);
+
+fun make_ctyp (Ctyp {cert, T, maxidx = _, sorts = _}) cargs =
+  let
+    val As = map typ_of cargs;
+    fun err () = raise TYPE ("make_ctyp", T :: As, []);
+  in
+    (case T of
+      Type (a, args) =>
+        Ctyp {
+          cert = fold join_certificate_ctyp cargs cert,
+          maxidx = fold maxidx_ctyp cargs ~1,
+          sorts = fold union_sorts_ctyp cargs [],
+          T = if length args = length cargs then Type (a, As) else err ()}
+    | _ => err ())
+  end;
+
 
 
 (** certified terms **)
@@ -454,6 +475,19 @@
        {cert = Context.Certificate_Id (Context.theory_id thy),
         tags = tags, maxidx = maxidx, shyps = shyps, hyps = hyps, tpairs = tpairs, prop = prop}));
 
+fun transfer_ctyp thy' cT =
+  let
+    val Ctyp {cert, T, maxidx, sorts} = cT;
+    val _ =
+      Context.subthy_id (Context.certificate_theory_id cert, Context.theory_id thy') orelse
+        raise CONTEXT ("Cannot transfer: not a super theory", [cT], [], [],
+          SOME (Context.Theory thy'));
+    val cert' = Context.join_certificate (Context.Certificate thy', cert);
+  in
+    if Context.eq_certificate (cert, cert') then cT
+    else Ctyp {cert = cert', T = T, maxidx = maxidx, sorts = sorts}
+  end;
+
 fun transfer_cterm thy' ct =
   let
     val Cterm {cert, t, T, maxidx, sorts} = ct;