equal
deleted
inserted
replaced
104 SOME (Bound j) |
104 SOME (Bound j) |
105 else if member (op =) fpTs T then |
105 else if member (op =) fpTs T then |
106 NONE |
106 NONE |
107 else if exists_subtype_in fpTs T then |
107 else if exists_subtype_in fpTs T then |
108 let val U = mk_U T in |
108 let val U = mk_U T in |
109 SOME (mk_to_nat_checked U $ (build_map ctxt [] (snd_const o fst) (T, U) $ Bound j)) |
109 SOME (mk_to_nat_checked U $ (build_map ctxt [] [] (snd_const o fst) (T, U) $ Bound j)) |
110 end |
110 end |
111 else |
111 else |
112 SOME (mk_to_nat_checked T $ Bound j); |
112 SOME (mk_to_nat_checked T $ Bound j); |
113 |
113 |
114 fun mk_arg n (k, arg_T) = |
114 fun mk_arg n (k, arg_T) = |