equal
deleted
inserted
replaced
105 if x = y then Type.constraint (uniform_typing x) (Type.constraint T (Bound lev)) |
105 if x = y then Type.constraint (uniform_typing x) (Type.constraint T (Bound lev)) |
106 else t |
106 else t |
107 | abs_body _ _ a = a; |
107 | abs_body _ _ a = a; |
108 fun close (y, U) B = |
108 fun close (y, U) B = |
109 let val B' = abs_body 0 y (Term.incr_boundvars 1 B) |
109 let val B' = abs_body 0 y (Term.incr_boundvars 1 B) |
110 in if Term.loose_bvar1 (B', 0) then Term.all dummyT $ Abs (y, U, B') else B end; |
110 in if Term.is_dependent B' then Term.all dummyT $ Abs (y, U, B') else B end; |
111 fun close_form A = |
111 fun close_form A = |
112 let |
112 let |
113 val occ_frees = rev (fold_aterms add_free A []); |
113 val occ_frees = rev (fold_aterms add_free A []); |
114 val bounds = xs @ map (rpair dummyT) (subtract (op =) commons occ_frees); |
114 val bounds = xs @ map (rpair dummyT) (subtract (op =) commons occ_frees); |
115 in fold_rev close bounds A end; |
115 in fold_rev close bounds A end; |