--- a/src/Pure/morphism.ML Fri Apr 21 15:30:59 2023 +0200
+++ b/src/Pure/morphism.ML Fri Apr 21 18:53:25 2023 +0200
@@ -22,6 +22,7 @@
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
@@ -82,6 +83,10 @@
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);