387 and of_univ bounds (Const (idx, ts)) typidx = |
387 and of_univ bounds (Const (idx, ts)) typidx = |
388 let |
388 let |
389 val ts' = take_until is_dict ts; |
389 val ts' = take_until is_dict ts; |
390 val c = const_of_idx idx; |
390 val c = const_of_idx idx; |
391 val (_, T) = Code.default_typscheme thy c; |
391 val (_, T) = Code.default_typscheme thy c; |
392 val T' = map_type_tvar (fn ((v, i), S) => TypeInfer.param (typidx + i) (v, [])) T; |
392 val T' = map_type_tfree (fn (v, _) => TypeInfer.param typidx (v, [])) T; |
393 val typidx' = typidx + maxidx_of_typ T' + 1; |
393 val typidx' = typidx + 1; |
394 in of_apps bounds (Term.Const (c, T'), ts') typidx' end |
394 in of_apps bounds (Term.Const (c, T'), ts') typidx' end |
395 | of_univ bounds (Free (name, ts)) typidx = |
395 | of_univ bounds (Free (name, ts)) typidx = |
396 of_apps bounds (Term.Free (name, dummyT), ts) typidx |
396 of_apps bounds (Term.Free (name, dummyT), ts) typidx |
397 | of_univ bounds (BVar (n, ts)) typidx = |
397 | of_univ bounds (BVar (n, ts)) typidx = |
398 of_apps bounds (Bound (bounds - n - 1), ts) typidx |
398 of_apps bounds (Bound (bounds - n - 1), ts) typidx |