equal
deleted
inserted
replaced
217 |
217 |
218 structure Data = Proof_Data |
218 structure Data = Proof_Data |
219 ( |
219 ( |
220 type T = data; |
220 type T = data; |
221 fun init thy = |
221 fun init thy = |
222 make_data (mode_default, Local_Syntax.init thy, |
222 make_data (mode_default, |
223 (Sign.tsig_of thy, Sign.tsig_of thy), |
223 Local_Syntax.init thy, |
224 (Sign.consts_of thy, Sign.consts_of thy), Facts.empty, empty_cases); |
224 (Type.change_ignore (Sign.tsig_of thy), Sign.tsig_of thy), |
|
225 (Consts.change_ignore (Sign.consts_of thy), Sign.consts_of thy), |
|
226 Facts.empty, |
|
227 empty_cases); |
225 ); |
228 ); |
226 |
229 |
227 fun rep_data ctxt = Data.get ctxt |> (fn Data rep => rep); |
230 fun rep_data ctxt = Data.get ctxt |> (fn Data rep => rep); |
228 |
231 |
229 fun map_data f = |
232 fun map_data f = |