383 #>> (fn ts' => list_comb (t, rev ts')) |
383 #>> (fn ts' => list_comb (t, rev ts')) |
384 and of_univ bounds (Const (idx, ts)) typidx = |
384 and of_univ bounds (Const (idx, ts)) typidx = |
385 let |
385 let |
386 val ts' = take_until is_dict ts; |
386 val ts' = take_until is_dict ts; |
387 val c = (the o Code_Name.const_rev thy o the o Inttab.lookup idx_tab) idx; |
387 val c = (the o Code_Name.const_rev thy o the o Inttab.lookup idx_tab) idx; |
388 val (_, T) = Code.default_typ thy c; |
388 val (_, T) = Code.default_typscheme thy c; |
389 val T' = map_type_tvar (fn ((v, i), S) => TypeInfer.param (typidx + i) (v, [])) T; |
389 val T' = map_type_tvar (fn ((v, i), S) => TypeInfer.param (typidx + i) (v, [])) T; |
390 val typidx' = typidx + maxidx_of_typ T' + 1; |
390 val typidx' = typidx + maxidx_of_typ T' + 1; |
391 in of_apps bounds (Term.Const (c, T'), ts') typidx' end |
391 in of_apps bounds (Term.Const (c, T'), ts') typidx' end |
392 | of_univ bounds (Free (name, ts)) typidx = |
392 | of_univ bounds (Free (name, ts)) typidx = |
393 of_apps bounds (Term.Free (name, dummyT), ts) typidx |
393 of_apps bounds (Term.Free (name, dummyT), ts) typidx |