# HG changeset patch # User wenzelm # Date 1393250320 -3600 # Node ID 9d605a21d7ec0b9572caa41e357ea015d17b2fa6 # Parent 601ea66c5bcdda5c878a0f032b8ae6edf926d92b prefer standard Proof_Context.transfer, with theory stamp transfer (should now work thanks to purely functional theory, without Theory.copy etc.); diff -r 601ea66c5bcd -r 9d605a21d7ec src/HOL/Tools/Nitpick/nitpick_model.ML --- a/src/HOL/Tools/Nitpick/nitpick_model.ML Mon Feb 24 13:52:48 2014 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_model.ML Mon Feb 24 14:58:40 2014 +0100 @@ -109,7 +109,7 @@ Mixfix (step_mixfix (), [1000], 1000)) thy in (pairself (pairself name_of) ((maybe_t, abs_t), (base_t, step_t)), - Proof_Context.transfer_syntax thy ctxt) + Proof_Context.transfer thy ctxt) end (** Term reconstruction **) diff -r 601ea66c5bcd -r 9d605a21d7ec src/Pure/Isar/proof_context.ML --- a/src/Pure/Isar/proof_context.ML Mon Feb 24 13:52:48 2014 +0100 +++ b/src/Pure/Isar/proof_context.ML Mon Feb 24 14:58:40 2014 +0100 @@ -50,7 +50,6 @@ val extern_const: Proof.context -> string -> xstring val markup_const: Proof.context -> string -> string val pretty_const: Proof.context -> string -> Pretty.T - val transfer_syntax: theory -> Proof.context -> Proof.context val transfer: theory -> Proof.context -> Proof.context val background_theory: (theory -> theory) -> Proof.context -> Proof.context val background_theory_result: (theory -> 'a * theory) -> Proof.context -> 'a * Proof.context diff -r 601ea66c5bcd -r 9d605a21d7ec src/Pure/Proof/proof_syntax.ML --- a/src/Pure/Proof/proof_syntax.ML Mon Feb 24 13:52:48 2014 +0100 +++ b/src/Pure/Proof/proof_syntax.ML Mon Feb 24 14:58:40 2014 +0100 @@ -246,7 +246,7 @@ fun pretty_proof ctxt prf = Proof_Context.pretty_term_abbrev - (Proof_Context.transfer_syntax (proof_syntax prf (Proof_Context.theory_of ctxt)) ctxt) + (Proof_Context.transfer (proof_syntax prf (Proof_Context.theory_of ctxt)) ctxt) (term_of_proof prf); fun pretty_proof_of ctxt full th =