# HG changeset patch
# User wenzelm
# Date 1176504380 -7200
# Node ID c803b2696ada4c893d7a656672a0af9395d4f9e9
# Parent  62857ad97cca334f403573ac2b30427903b2cc8d
added Morphism.transform/form (generic non-sense);

diff -r 62857ad97cca -r c803b2696ada src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Sat Apr 14 00:46:20 2007 +0200
+++ b/src/Pure/Isar/proof_context.ML	Sat Apr 14 00:46:20 2007 +0200
@@ -921,7 +921,7 @@
     Context.mapping_result
       (Sign.add_abbrev Syntax.internalM arg') (add_abbrev Syntax.internalM arg')
     #-> (fn (lhs, _) =>
-      Term.equiv_types (rhs, rhs') ? target_notation prmode [(lhs, mx)] Morphism.identity)
+      Term.equiv_types (rhs, rhs') ? Morphism.form (target_notation prmode [(lhs, mx)]))
   end;
 
 fun local_abbrev (x, rhs) =
diff -r 62857ad97cca -r c803b2696ada src/Pure/morphism.ML
--- a/src/Pure/morphism.ML	Sat Apr 14 00:46:20 2007 +0200
+++ b/src/Pure/morphism.ML	Sat Apr 14 00:46:20 2007 +0200
@@ -37,6 +37,8 @@
   val thm_morphism: (thm -> thm) -> morphism
   val identity: morphism
   val compose: morphism -> morphism -> morphism
+  val transform: morphism -> (morphism -> 'a) -> morphism -> 'a
+  val form: (morphism -> 'a) -> 'a
 end;
 
 structure Morphism: MORPHISM =
@@ -76,6 +78,9 @@
 
 fun phi1 $> phi2 = compose phi2 phi1;
 
+fun transform phi f = fn psi => f (phi $> psi);
+fun form f = f identity;
+
 end;
 
 structure BasicMorphism: BASIC_MORPHISM = Morphism;