# 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 =