# HG changeset patch
# User wenzelm
# Date 1170622935 -3600
# Node ID 6eac7f7c32945e23c037cd92c24cd5b7795523dd
# Parent  52ba19aaa9c2385920775c0143612a66bb8eb293
added cterm interface;

diff -r 52ba19aaa9c2 -r 6eac7f7c3294 src/Pure/morphism.ML
--- 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;