136 val ((RepC, AbsC), consts_lthy) = lthy |
136 val ((RepC, AbsC), consts_lthy) = lthy |
137 |> Local_Theory.background_theory_result |
137 |> Local_Theory.background_theory_result |
138 (Sign.declare_const lthy ((Rep_name, newT --> oldT), NoSyn) ##>> |
138 (Sign.declare_const lthy ((Rep_name, newT --> oldT), NoSyn) ##>> |
139 Sign.declare_const lthy ((Abs_name, oldT --> newT), NoSyn)); |
139 Sign.declare_const lthy ((Abs_name, oldT --> newT), NoSyn)); |
140 val const_dep = Theory.const_dep (Proof_Context.theory_of consts_lthy); |
140 val const_dep = Theory.const_dep (Proof_Context.theory_of consts_lthy); |
|
141 val defs_context = Proof_Context.defs_context consts_lthy; |
141 |
142 |
142 val A_consts = fold_aterms (fn Const c => insert (op =) (const_dep c) | _ => I) A []; |
143 val A_consts = fold_aterms (fn Const c => insert (op =) (const_dep c) | _ => I) A []; |
143 val A_types = |
144 val A_types = |
144 (fold_types o fold_subtypes) (fn Type t => insert (op =) (Theory.type_dep t) | _ => I) A []; |
145 (fold_types o fold_subtypes) (fn Type t => insert (op =) (Theory.type_dep t) | _ => I) A []; |
145 val typedef_deps = A_consts @ A_types; |
146 val typedef_deps = A_consts @ A_types; |
147 val newT_dep = Theory.type_dep (dest_Type newT); |
148 val newT_dep = Theory.type_dep (dest_Type newT); |
148 |
149 |
149 val ((axiom_name, axiom), axiom_lthy) = consts_lthy |
150 val ((axiom_name, axiom), axiom_lthy) = consts_lthy |
150 |> Local_Theory.background_theory_result |
151 |> Local_Theory.background_theory_result |
151 (Thm.add_axiom consts_lthy (type_definition_name, mk_typedef newT oldT RepC AbsC A) ##> |
152 (Thm.add_axiom consts_lthy (type_definition_name, mk_typedef newT oldT RepC AbsC A) ##> |
152 Theory.add_deps consts_lthy "" newT_dep typedef_deps ##> |
153 Theory.add_deps defs_context "" newT_dep typedef_deps ##> |
153 Theory.add_deps consts_lthy "" (const_dep (dest_Const RepC)) [newT_dep] ##> |
154 Theory.add_deps defs_context "" (const_dep (dest_Const RepC)) [newT_dep] ##> |
154 Theory.add_deps consts_lthy "" (const_dep (dest_Const AbsC)) [newT_dep]); |
155 Theory.add_deps defs_context "" (const_dep (dest_Const AbsC)) [newT_dep]); |
155 |
156 |
156 val axiom_defs = Theory.defs_of (Proof_Context.theory_of axiom_lthy); |
157 val axiom_defs = Theory.defs_of (Proof_Context.theory_of axiom_lthy); |
157 val newT_deps = maps #2 (Defs.get_deps axiom_defs (#1 newT_dep)); |
158 val newT_deps = maps #2 (Defs.get_deps axiom_defs (#1 newT_dep)); |
158 val _ = |
159 val _ = |
159 if null newT_deps orelse overloaded orelse Config.get lthy typedef_overloaded then () |
160 if null newT_deps orelse overloaded orelse Config.get lthy typedef_overloaded then () |
164 [Pretty.brk 1, Pretty.str "\"", Pretty.keyword1 "typedef", Pretty.brk 1, |
165 [Pretty.brk 1, Pretty.str "\"", Pretty.keyword1 "typedef", Pretty.brk 1, |
165 Pretty.str "(", Pretty.keyword2 "overloaded", Pretty.str ")\"", Pretty.brk 1] @ |
166 Pretty.str "(", Pretty.keyword2 "overloaded", Pretty.str ")\"", Pretty.brk 1] @ |
166 Pretty.text "or enable configuration option \"typedef_overloaded\" in the context."), |
167 Pretty.text "or enable configuration option \"typedef_overloaded\" in the context."), |
167 Pretty.block [Pretty.str " Type:", Pretty.brk 2, Syntax.pretty_typ axiom_lthy newT], |
168 Pretty.block [Pretty.str " Type:", Pretty.brk 2, Syntax.pretty_typ axiom_lthy newT], |
168 Pretty.block (Pretty.str " Deps:" :: Pretty.brk 2 :: |
169 Pretty.block (Pretty.str " Deps:" :: Pretty.brk 2 :: |
169 Pretty.commas (map (Defs.pretty_entry axiom_lthy) newT_deps))])) |
170 Pretty.commas |
|
171 (map (Defs.pretty_entry (Proof_Context.defs_context axiom_lthy)) newT_deps))])) |
170 in ((RepC, AbsC, axiom_name, axiom), axiom_lthy) end; |
172 in ((RepC, AbsC, axiom_name, axiom), axiom_lthy) end; |
171 |
173 |
172 |
174 |
173 (* derived bindings *) |
175 (* derived bindings *) |
174 |
176 |