223 |
223 |
224 (* declarations *) |
224 (* declarations *) |
225 |
225 |
226 fun declare authentic naming tags (c, declT) = map_consts (fn (decls, constraints, rev_abbrevs) => |
226 fun declare authentic naming tags (c, declT) = map_consts (fn (decls, constraints, rev_abbrevs) => |
227 let |
227 let |
228 val decl = {T = declT, typargs = typargs_of declT, tags = tags, authentic = authentic}; |
228 val tags' = tags |> Position.default_properties (Position.thread_data ()); |
|
229 val decl = {T = declT, typargs = typargs_of declT, tags = tags', authentic = authentic}; |
229 val decls' = decls |> extend_decls naming (c, ((decl, NONE), serial ())); |
230 val decls' = decls |> extend_decls naming (c, ((decl, NONE), serial ())); |
230 in (decls', constraints, rev_abbrevs) end); |
231 in (decls', constraints, rev_abbrevs) end); |
231 |
232 |
232 |
233 |
233 (* constraints *) |
234 (* constraints *) |
279 val _ = Term.exists_subterm Term.is_Var rhs andalso err "Illegal schematic variables"; |
280 val _ = Term.exists_subterm Term.is_Var rhs andalso err "Illegal schematic variables"; |
280 val _ = null (Term.hidden_polymorphism rhs) orelse err "Extra type variables"; |
281 val _ = null (Term.hidden_polymorphism rhs) orelse err "Extra type variables"; |
281 in |
282 in |
282 consts |> map_consts (fn (decls, constraints, rev_abbrevs) => |
283 consts |> map_consts (fn (decls, constraints, rev_abbrevs) => |
283 let |
284 let |
284 val decl = {T = T, typargs = typargs_of T, tags = tags, authentic = true}; |
285 val tags' = tags |> Position.default_properties (Position.thread_data ()); |
|
286 val decl = {T = T, typargs = typargs_of T, tags = tags', authentic = true}; |
285 val abbr = {rhs = rhs, normal_rhs = normal_rhs, force_expand = force_expand}; |
287 val abbr = {rhs = rhs, normal_rhs = normal_rhs, force_expand = force_expand}; |
286 val decls' = decls |
288 val decls' = decls |
287 |> extend_decls naming (c, ((decl, SOME abbr), serial ())); |
289 |> extend_decls naming (c, ((decl, SOME abbr), serial ())); |
288 val rev_abbrevs' = rev_abbrevs |
290 val rev_abbrevs' = rev_abbrevs |
289 |> fold (curry Symtab.cons_list mode) (rev_abbrev lhs rhs); |
291 |> fold (curry Symtab.cons_list mode) (rev_abbrev lhs rhs); |