src/Pure/morphism.ML

--- a/src/Pure/morphism.ML	Sat Jul 28 22:01:01 2007 +0200
+++ b/src/Pure/morphism.ML	Sat Jul 28 22:01:06 2007 +0200
@@ -10,6 +10,7 @@
 signature BASIC_MORPHISM =
 sig
   type morphism
+  type declaration = morphism -> Context.generic -> Context.generic
   val $> : morphism * morphism -> morphism
 end
 
@@ -51,6 +52,8 @@
   term: term -> term,
   fact: thm list -> thm list};
 
+type declaration = morphism -> Context.generic -> Context.generic;
+
 fun name (Morphism {name, ...}) = name;
 fun var (Morphism {var, ...}) = var;
 fun typ (Morphism {typ, ...}) = typ;