src/Pure/morphism.ML

   val name: morphism -> string -> string
   val typ: morphism -> typ -> typ
   val term: morphism -> term -> term
   val fact: morphism -> thm list -> thm list
   val thm: morphism -> thm -> thm
+  val cterm: morphism -> cterm -> cterm
   val morphism:
    {name: string -> string,
     var: string * mixfix -> string * mixfix,
     typ: typ -> typ,
     term: term -> term,

 fun var (Morphism {var, ...}) = var;
 fun typ (Morphism {typ, ...}) = typ;
 fun term (Morphism {term, ...}) = term;
 fun fact (Morphism {fact, ...}) = fact;
 val thm = singleton o fact;
+val cterm = Drule.cterm_rule o thm;
 
 val morphism = Morphism;
 
 fun name_morphism name = morphism {name = name, var = I, typ = I, term = I, fact = I};
 fun var_morphism var = morphism {name = I, var = var, typ = I, term = I, fact = I};