--- a/src/Pure/envir.ML Sun Apr 13 16:40:02 2008 +0200
+++ b/src/Pure/envir.ML Sun Apr 13 16:40:04 2008 +0200
@@ -13,6 +13,7 @@
type tenv
datatype env = Envir of {asol: tenv, iTs: Type.tyenv, maxidx: int}
val type_env: env -> Type.tyenv
+ val insert_sorts: env -> sort list -> sort list
exception SAME
val genvars: string -> env * typ list -> env * term list
val genvar: string -> env * typ -> env * term
@@ -58,6 +59,9 @@
fun type_env (Envir {iTs, ...}) = iTs;
+(*NB: type unification may invent new sorts*)
+val insert_sorts = Vartab.fold (fn (_, (_, T)) => Sorts.insert_typ T) o type_env;
+
(*Generate a list of distinct variables.
Increments index to make them distinct from ALL present variables. *)
fun genvars name (Envir{maxidx, asol, iTs}, Ts) : env * term list =