# HG changeset patch
# User wenzelm
# Date 1176672354 -7200
# Node ID 0b18739c3e81359994b653bc442478ddec6b96de
# Parent  f44439cdce776e2ac0f00dbf1dd4545a52098aaa
removed obsolete redeclare_skolems;

diff -r f44439cdce77 -r 0b18739c3e81 src/Pure/variable.ML
--- a/src/Pure/variable.ML	Sun Apr 15 23:25:52 2007 +0200
+++ b/src/Pure/variable.ML	Sun Apr 15 23:25:54 2007 +0200
@@ -168,14 +168,6 @@
 
 (* constraints *)
 
-fun redeclare_skolems ctxt = ctxt |> map_constraints (apfst (fn types =>
-  let
-    fun decl (x, x') =
-      (case default_type ctxt x' of
-        SOME T => Vartab.update ((x, ~1), T)
-      | 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);
 
@@ -190,8 +182,7 @@
         | TVar v => constrain_tvar v
         | _ => I)) t sorts;
   in (types', sorts') end)
-  #> declare_type_names t
-  #> redeclare_skolems;
+  #> declare_type_names t;
 
 
 (* common declarations *)