removed obsolete redeclare_skolems;
authorwenzelm
Sun Apr 15 23:25:54 2007 +0200 (2007-04-15)
changeset 227110b18739c3e81
parent 22710 f44439cdce77
child 22712 8f2ba236918b
removed obsolete redeclare_skolems;
src/Pure/variable.ML
     1.1 --- a/src/Pure/variable.ML	Sun Apr 15 23:25:52 2007 +0200
     1.2 +++ b/src/Pure/variable.ML	Sun Apr 15 23:25:54 2007 +0200
     1.3 @@ -168,14 +168,6 @@
     1.4  
     1.5  (* constraints *)
     1.6  
     1.7 -fun redeclare_skolems ctxt = ctxt |> map_constraints (apfst (fn types =>
     1.8 -  let
     1.9 -    fun decl (x, x') =
    1.10 -      (case default_type ctxt x' of
    1.11 -        SOME T => Vartab.update ((x, ~1), T)
    1.12 -      | NONE => I);
    1.13 -  in fold_rev decl (fixes_of ctxt) types end));
    1.14 -
    1.15  fun constrain_tvar (xi, S) =
    1.16    if S = dummyS then Vartab.delete_safe xi else Vartab.update (xi, S);
    1.17  
    1.18 @@ -190,8 +182,7 @@
    1.19          | TVar v => constrain_tvar v
    1.20          | _ => I)) t sorts;
    1.21    in (types', sorts') end)
    1.22 -  #> declare_type_names t
    1.23 -  #> redeclare_skolems;
    1.24 +  #> declare_type_names t;
    1.25  
    1.26  
    1.27  (* common declarations *)