src/Pure/morphism.ML

   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

     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));
 
 val _ = ML_system_pp (fn _ => fn _ => Pretty.to_polyml o pretty);