added cterm interface;

--- a/src/Pure/morphism.ML	Sun Feb 04 22:02:14 2007 +0100
+++ b/src/Pure/morphism.ML	Sun Feb 04 22:02:15 2007 +0100
@@ -22,6 +22,7 @@
   val term: morphism -> term -> term
   val fact: morphism -> thm list -> thm list
   val thm: morphism -> thm -> thm
+  val cterm: morphism -> cterm -> cterm
   val morphism:
    {name: string -> string,
     var: string * mixfix -> string * mixfix,
@@ -54,6 +55,7 @@
 fun term (Morphism {term, ...}) = term;
 fun fact (Morphism {fact, ...}) = fact;
 val thm = singleton o fact;
+val cterm = Drule.cterm_rule o thm;
 
 val morphism = Morphism;