# HG changeset patch
# User wenzelm
# Date 882962466 -3600
# Node ID d26e28c52788a46bd8f1c8ed15e6f7bdd6f2399e
# Parent  708d7c26db5b9f7970a5e2b2e435784dbd8259b0
export range_type;

diff -r 708d7c26db5b -r d26e28c52788 src/Pure/term.ML
--- a/src/Pure/term.ML	Wed Dec 24 12:20:54 1997 +0100
+++ b/src/Pure/term.ML	Wed Dec 24 12:21:06 1997 +0100
@@ -24,6 +24,7 @@
   val ---> : typ list * typ -> typ
   val is_TVar: typ -> bool
   val domain_type: typ -> typ
+  val range_type: typ -> typ
   val binder_types: typ -> typ list
   val body_type: typ -> typ
   val strip_type: typ -> typ list * typ