48 val pretty_type: Proof.context -> string -> Pretty.T |
48 val pretty_type: Proof.context -> string -> Pretty.T |
49 val extern_const: Proof.context -> string -> xstring |
49 val extern_const: Proof.context -> string -> xstring |
50 val markup_const: Proof.context -> string -> string |
50 val markup_const: Proof.context -> string -> string |
51 val pretty_const: Proof.context -> string -> Pretty.T |
51 val pretty_const: Proof.context -> string -> Pretty.T |
52 val transfer: theory -> Proof.context -> Proof.context |
52 val transfer: theory -> Proof.context -> Proof.context |
|
53 val transfer_facts: theory -> Proof.context -> Proof.context |
53 val background_theory: (theory -> theory) -> Proof.context -> Proof.context |
54 val background_theory: (theory -> theory) -> Proof.context -> Proof.context |
54 val background_theory_result: (theory -> 'a * theory) -> Proof.context -> 'a * Proof.context |
55 val background_theory_result: (theory -> 'a * theory) -> Proof.context -> 'a * Proof.context |
55 val facts_of: Proof.context -> Facts.T |
56 val facts_of: Proof.context -> Facts.T |
56 val facts_of_fact: Proof.context -> string -> Facts.T |
57 val facts_of_fact: Proof.context -> string -> Facts.T |
57 val markup_extern_fact: Proof.context -> string -> Markup.T * xstring |
58 val markup_extern_fact: Proof.context -> string -> Markup.T * xstring |
321 fun transfer_syntax thy ctxt = ctxt |> |
322 fun transfer_syntax thy ctxt = ctxt |> |
322 map_syntax (Local_Syntax.rebuild thy) |> |
323 map_syntax (Local_Syntax.rebuild thy) |> |
323 map_tsig (fn tsig as (local_tsig, global_tsig) => |
324 map_tsig (fn tsig as (local_tsig, global_tsig) => |
324 let val thy_tsig = Sign.tsig_of thy in |
325 let val thy_tsig = Sign.tsig_of thy in |
325 if Type.eq_tsig (thy_tsig, global_tsig) then tsig |
326 if Type.eq_tsig (thy_tsig, global_tsig) then tsig |
326 else (Type.merge_tsig (Context.pretty ctxt) (local_tsig, thy_tsig), thy_tsig) |
327 else (Type.merge_tsig (Context.pretty ctxt) (local_tsig, thy_tsig), thy_tsig) (*historic merge order*) |
327 end) |> |
328 end) |> |
328 map_consts (fn consts as (local_consts, global_consts) => |
329 map_consts (fn consts as (local_consts, global_consts) => |
329 let val thy_consts = Sign.consts_of thy in |
330 let val thy_consts = Sign.consts_of thy in |
330 if Consts.eq_consts (thy_consts, global_consts) then consts |
331 if Consts.eq_consts (thy_consts, global_consts) then consts |
331 else (Consts.merge (local_consts, thy_consts), thy_consts) |
332 else (Consts.merge (local_consts, thy_consts), thy_consts) (*historic merge order*) |
332 end); |
333 end); |
333 |
334 |
334 fun transfer thy = Context.raw_transfer thy #> transfer_syntax thy; |
335 fun transfer thy = Context.raw_transfer thy #> transfer_syntax thy; |
|
336 |
|
337 fun transfer_facts thy = |
|
338 map_facts (fn local_facts => Facts.merge (Global_Theory.facts_of thy, local_facts)); |
335 |
339 |
336 fun background_theory f ctxt = transfer (f (theory_of ctxt)) ctxt; |
340 fun background_theory f ctxt = transfer (f (theory_of ctxt)) ctxt; |
337 |
341 |
338 fun background_theory_result f ctxt = |
342 fun background_theory_result f ctxt = |
339 let val (res, thy') = f (theory_of ctxt) |
343 let val (res, thy') = f (theory_of ctxt) |