# HG changeset patch
# User wenzelm
# Date 1460382618 -7200
# Node ID 2fd4378caca2dad9cccc2fcf205e736e9eadb196
# Parent  c5d0fdc260faf755d857848e9dab9bbaedc76056
back to dummy constraints (amending dd2914250ca7): important for Syntax_Phases.get_free/is_declared;

diff -r c5d0fdc260fa -r 2fd4378caca2 src/Pure/variable.ML
--- a/src/Pure/variable.ML	Mon Apr 11 15:26:58 2016 +0200
+++ b/src/Pure/variable.ML	Mon Apr 11 15:50:18 2016 +0200
@@ -230,9 +230,6 @@
 
 (* constraints *)
 
-fun constrain_var (xi, T) =
-  if T = dummyT then Vartab.delete_safe xi else Vartab.update (xi, T);
-
 fun constrain_tvar (xi, raw_S) =
   let val S = #2 (Term_Position.decode_positionS raw_S)
   in if S = dummyS then Vartab.delete_safe xi else Vartab.update (xi, S) end;
@@ -240,8 +237,8 @@
 fun declare_constraints t = map_constraints (fn (types, sorts) =>
   let
     val types' = fold_aterms
-      (fn Free (x, T) => constrain_var ((x, ~1), T)
-        | Var v => constrain_var v
+      (fn Free (x, T) => Vartab.update ((x, ~1), T)
+        | Var v => Vartab.update v
         | _ => I) t types;
     val sorts' = (fold_types o fold_atyps)
       (fn TFree (x, S) => constrain_tvar ((x, ~1), S)