prefer standard Proof_Context.transfer, with theory stamp transfer (should now work thanks to purely functional theory, without Theory.copy etc.);
--- 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 **)
--- 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
--- 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 =