# HG changeset patch
# User wenzelm
# Date 931287837 -7200
# Node ID 5e20ddfdf3c7a53e760b9b6f0da214521879ddeb
# Parent  29060d9b60d4926262164ba2dca15c146b729bd5
export term_of_typ;

diff -r 29060d9b60d4 -r 5e20ddfdf3c7 src/Pure/Syntax/type_ext.ML
--- a/src/Pure/Syntax/type_ext.ML	Tue Jul 06 21:03:34 1999 +0200
+++ b/src/Pure/Syntax/type_ext.ML	Tue Jul 06 21:03:57 1999 +0200
@@ -10,13 +10,13 @@
 sig
   val raw_term_sorts: term -> (indexname * sort) list
   val typ_of_term: (indexname -> sort) -> term -> typ
+  val term_of_typ: bool -> typ -> term
 end;
 
 signature TYPE_EXT =
 sig
   include TYPE_EXT0
   val term_of_sort: sort -> term
-  val term_of_typ: bool -> typ -> term
   val tappl_ast_tr': Ast.ast * Ast.ast list -> Ast.ast
   val type_ext: SynExt.syn_ext
 end;