96 fun add_typ T proper (cx as (names, typs, terms)) = |
96 fun add_typ T proper (cx as (names, typs, terms)) = |
97 (case Typtab.lookup typs T of |
97 (case Typtab.lookup typs T of |
98 SOME (name, _) => (name, cx) |
98 SOME (name, _) => (name, cx) |
99 | NONE => |
99 | NONE => |
100 let |
100 let |
101 val sugg = Name.desymbolize true (suggested_name_of_typ T) ^ safe_suffix |
101 val sugg = Name.desymbolize (SOME true) (suggested_name_of_typ T) ^ safe_suffix |
102 val (name, names') = Name.variant sugg names |
102 val (name, names') = Name.variant sugg names |
103 val typs' = Typtab.update (T, (name, proper)) typs |
103 val typs' = Typtab.update (T, (name, proper)) typs |
104 in (name, (names', typs', terms)) end) |
104 in (name, (names', typs', terms)) end) |
105 |
105 |
106 fun add_fun t sort (cx as (names, typs, terms)) = |
106 fun add_fun t sort (cx as (names, typs, terms)) = |
107 (case Termtab.lookup terms t of |
107 (case Termtab.lookup terms t of |
108 SOME (name, _) => (name, cx) |
108 SOME (name, _) => (name, cx) |
109 | NONE => |
109 | NONE => |
110 let |
110 let |
111 val sugg = Name.desymbolize false (suggested_name_of_term t) ^ safe_suffix |
111 val sugg = Name.desymbolize (SOME false) (suggested_name_of_term t) ^ safe_suffix |
112 val (name, names') = Name.variant sugg names |
112 val (name, names') = Name.variant sugg names |
113 val terms' = Termtab.update (t, (name, sort)) terms |
113 val terms' = Termtab.update (t, (name, sort)) terms |
114 in (name, (names', typs, terms')) end) |
114 in (name, (names', typs, terms')) end) |
115 |
115 |
116 fun sign_of header dtyps (_, typs, terms) = { |
116 fun sign_of header dtyps (_, typs, terms) = { |