# HG changeset patch
# User wenzelm
# Date 1208097604 -7200
# Node ID 1d5d42d8fd66249157f54686c4ae6d9bdb089230
# Parent  0bfccafc52ebd6f248e3a1153849efeea6adc5b8
added insert_sorts (from thm.ML);

diff -r 0bfccafc52eb -r 1d5d42d8fd66 src/Pure/envir.ML
--- 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 =