--- a/src/Pure/variable.ML Tue Nov 14 00:15:43 2006 +0100
+++ b/src/Pure/variable.ML Tue Nov 14 00:16:30 2006 +0100
@@ -172,6 +172,9 @@
| NONE => I);
in fold_rev decl (fixes_of ctxt) types end));
+fun constrain_tvar (xi, S) =
+ if S = dummyS then Vartab.delete_safe xi else Vartab.update (xi, S);
+
fun declare_constraints t = map_constraints (fn (types, sorts) =>
let
val types' = fold_aterms
@@ -179,8 +182,8 @@
| Var v => Vartab.update v
| _ => I) t types;
val sorts' = fold_types (fold_atyps
- (fn TFree (x, S) => Vartab.update ((x, ~1), S)
- | TVar v => Vartab.update v
+ (fn TFree (x, S) => constrain_tvar ((x, ~1), S)
+ | TVar v => constrain_tvar v
| _ => I)) t sorts;
in (types', sorts') end)
#> declare_type_names t