diff --git a/src/Pure/morphism.ML b/src/Pure/morphism.ML
--- a/src/Pure/morphism.ML
+++ b/src/Pure/morphism.ML
@@ -1,175 +1,180 @@
 (*  Title:      Pure/morphism.ML
     Author:     Makarius
 
 Abstract morphisms on formal entities.
 *)
 
 infix 1 $>
 
 signature BASIC_MORPHISM =
 sig
   type morphism
   type declaration = morphism -> Context.generic -> Context.generic
   val $> : morphism * morphism -> morphism
 end
 
 signature MORPHISM =
 sig
   include BASIC_MORPHISM
   exception MORPHISM of string * exn
   val morphism: string ->
    {binding: (binding -> binding) list,
     typ: (typ -> typ) list,
     term: (term -> term) list,
     fact: (thm list -> thm list) list} -> morphism
   val is_identity: morphism -> bool
   val pretty: morphism -> Pretty.T
   val binding: morphism -> binding -> binding
   val binding_prefix: morphism -> (string * bool) list
   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 identity: morphism
   val compose: morphism -> morphism -> morphism
   val transform: morphism -> (morphism -> 'a) -> morphism -> 'a
   val form: (morphism -> 'a) -> 'a
   val binding_morphism: string -> (binding -> binding) -> morphism
   val typ_morphism: string -> (typ -> typ) -> morphism
   val term_morphism: string -> (term -> term) -> morphism
   val fact_morphism: string -> (thm list -> thm list) -> morphism
   val thm_morphism: string -> (thm -> thm) -> morphism
   val transfer_morphism: theory -> morphism
   val transfer_morphism': Proof.context -> morphism
   val transfer_morphism'': Context.generic -> morphism
   val trim_context_morphism: morphism
   val instantiate_frees_morphism: ctyp TFrees.table * cterm Frees.table -> morphism
   val instantiate_morphism: ctyp TVars.table * cterm Vars.table -> morphism
 end;
 
 structure Morphism: MORPHISM =
 struct
 
 (* named functions *)
 
 type 'a funs = (string * ('a -> 'a)) list;
 
 exception MORPHISM of string * exn;
 
 fun app (name, f) x = f x
   handle exn =>
     if Exn.is_interrupt exn then Exn.reraise exn else raise MORPHISM (name, exn);
 
 fun apply fs = fold_rev app fs;
 
 
 (* type morphism *)
 
 datatype morphism = Morphism of
  {names: string list,
   binding: binding funs,
   typ: typ funs,
   term: term funs,
   fact: thm list funs};
 
+fun rep (Morphism args) = args;
+
 type declaration = morphism -> Context.generic -> Context.generic;
 
 fun morphism a {binding, typ, term, fact} =
   Morphism {
     names = if a = "" then [] else [a],
     binding = map (pair a) binding,
     typ = map (pair a) typ,
     term = map (pair a) term,
     fact = map (pair a) fact};
 
 (*syntactic test only!*)
 fun is_identity (Morphism {names, binding, typ, term, fact}) =
   null names andalso null binding andalso null typ andalso null term andalso null fact;
 
-fun pretty (Morphism {names, ...}) = Pretty.enum ";" "{" "}" (map Pretty.str (rev names));
+fun pretty phi = Pretty.enum ";" "{" "}" (map Pretty.str (rev (#names (rep phi))));
 
 val _ = ML_system_pp (fn _ => fn _ => Pretty.to_polyml o pretty);
 
-fun binding (Morphism {binding, ...}) = apply binding;
+val binding = apply o #binding o rep;
 fun binding_prefix morph = Binding.name "x" |> binding morph |> Binding.prefix_of;
-fun typ (Morphism {typ, ...}) = apply typ;
-fun term (Morphism {term, ...}) = apply term;
-fun fact (Morphism {fact, ...}) = apply fact;
+val typ = apply o #typ o rep;
+val term = apply o #term o rep;
+val fact = apply o #fact o rep;
 val thm = singleton o fact;
 val cterm = Drule.cterm_rule o thm;
 
 
 (* morphism combinators *)
 
 val identity = morphism "" {binding = [], typ = [], term = [], fact = []};
 
-fun compose
-    (Morphism {names = names1, binding = binding1, typ = typ1, term = term1, fact = fact1})
-    (Morphism {names = names2, binding = binding2, typ = typ2, term = term2, fact = fact2}) =
-  Morphism {
-    names = names1 @ names2,
-    binding = binding1 @ binding2,
-    typ = typ1 @ typ2,
-    term = term1 @ term2,
-    fact = fact1 @ fact2};
+fun compose phi1 phi2 =
+  let
+    val {names = names1, binding = binding1, typ = typ1, term = term1, fact = fact1} = rep phi1;
+    val {names = names2, binding = binding2, typ = typ2, term = term2, fact = fact2} = rep phi2;
+  in
+    Morphism {
+      names = names1 @ names2,
+      binding = binding1 @ binding2,
+      typ = typ1 @ typ2,
+      term = term1 @ term2,
+      fact = fact1 @ fact2}
+  end;
 
 fun phi1 $> phi2 = compose phi2 phi1;
 
 fun transform phi f = fn psi => f (phi $> psi);
 fun form f = f identity;
 
 
 (* concrete morphisms *)
 
 fun binding_morphism a binding = morphism a {binding = [binding], typ = [], term = [], fact = []};
 fun typ_morphism a typ = morphism a {binding = [], typ = [typ], term = [], fact = []};
 fun term_morphism a term = morphism a {binding = [], typ = [], term = [term], fact = []};
 fun fact_morphism a fact = morphism a {binding = [], typ = [], term = [], fact = [fact]};
 fun thm_morphism a thm = morphism a {binding = [], typ = [], term = [], fact = [map thm]};
 
 val transfer_morphism = thm_morphism "transfer" o Thm.join_transfer;
 val transfer_morphism' = transfer_morphism o Proof_Context.theory_of;
 val transfer_morphism'' = transfer_morphism o Context.theory_of;
 
 val trim_context_morphism = thm_morphism "trim_context" Thm.trim_context;
 
 
 (* instantiate *)
 
 fun instantiate_frees_morphism (cinstT, cinst) =
   if TFrees.is_empty cinstT andalso Frees.is_empty cinst then identity
   else
     let
       val instT = TFrees.map (K Thm.typ_of) cinstT;
       val inst = Frees.map (K Thm.term_of) cinst;
     in
       morphism "instantiate_frees"
         {binding = [],
          typ =
           if TFrees.is_empty instT then []
           else [Term_Subst.instantiateT_frees instT],
          term = [Term_Subst.instantiate_frees (instT, inst)],
          fact = [map (Thm.instantiate_frees (cinstT, cinst))]}
     end;
 
 fun instantiate_morphism (cinstT, cinst) =
   if TVars.is_empty cinstT andalso Vars.is_empty cinst then identity
   else
     let
       val instT = TVars.map (K Thm.typ_of) cinstT;
       val inst = Vars.map (K Thm.term_of) cinst;
     in
       morphism "instantiate"
         {binding = [],
          typ =
           if TVars.is_empty instT then []
           else [Term_Subst.instantiateT instT],
          term = [Term_Subst.instantiate (instT, inst)],
          fact = [map (Thm.instantiate (cinstT, cinst))]}
     end;
 
 end;
 
 structure Basic_Morphism: BASIC_MORPHISM = Morphism;
 open Basic_Morphism;