equal
deleted
inserted
replaced
87 val commons = map #1 xs; |
87 val commons = map #1 xs; |
88 val _ = |
88 val _ = |
89 (case duplicates (op =) commons of [] => () |
89 (case duplicates (op =) commons of [] => () |
90 | dups => error ("Duplicate local variables " ^ commas_quote dups)); |
90 | dups => error ("Duplicate local variables " ^ commas_quote dups)); |
91 val frees = rev ((fold o fold_aterms) add_free As (rev commons)); |
91 val frees = rev ((fold o fold_aterms) add_free As (rev commons)); |
92 val types = map (TypeInfer.param i o rpair []) (Name.invents Name.context "'a" (length frees)); |
92 val types = map (TypeInfer.param i o rpair []) (Name.invents Name.context Name.aT (length frees)); |
93 val uniform_typing = the o AList.lookup (op =) (frees ~~ types); |
93 val uniform_typing = the o AList.lookup (op =) (frees ~~ types); |
94 |
94 |
95 fun abs_body lev y (Abs (x, T, b)) = Abs (x, T, abs_body (lev + 1) y b) |
95 fun abs_body lev y (Abs (x, T, b)) = Abs (x, T, abs_body (lev + 1) y b) |
96 | abs_body lev y (t $ u) = abs_body lev y t $ abs_body lev y u |
96 | abs_body lev y (t $ u) = abs_body lev y t $ abs_body lev y u |
97 | abs_body lev y (t as Free (x, T)) = |
97 | abs_body lev y (t as Free (x, T)) = |