--- 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 *)