# HG changeset patch
# User wenzelm
# Date 1682096005 -7200
# Node ID 01d6b2a44df8070325c0ca0fdfaa9f5c126f4233
# Parent  5728d5ebce34e8be622701d7b746653c737fdde0
more operations;

diff -r 5728d5ebce34 -r 01d6b2a44df8 src/Pure/morphism.ML
--- 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);