# HG changeset patch
# User wenzelm
# Date 1163459790 -3600
# Node ID 5c1b1ae737e11fd779f4364775f18b5f68a26c3b
# Parent  2207380f75764ed0e7c1469640e8960c7382a5f3
declare_constraints: reset constraint on dummyS;

diff -r 2207380f7576 -r 5c1b1ae737e1 src/Pure/variable.ML
--- 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