prefer standard Proof_Context.transfer, with theory stamp transfer (should now work thanks to purely functional theory, without Theory.copy etc.);
authorwenzelm
Mon Feb 24 14:58:40 2014 +0100 (2014-02-24)
changeset 557259d605a21d7ec
parent 55717 601ea66c5bcd
child 55726 945ad7eaf37f
prefer standard Proof_Context.transfer, with theory stamp transfer (should now work thanks to purely functional theory, without Theory.copy etc.);
src/HOL/Tools/Nitpick/nitpick_model.ML
src/Pure/Isar/proof_context.ML
src/Pure/Proof/proof_syntax.ML
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick_model.ML	Mon Feb 24 13:52:48 2014 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_model.ML	Mon Feb 24 14:58:40 2014 +0100
     1.3 @@ -109,7 +109,7 @@
     1.4                            Mixfix (step_mixfix (), [1000], 1000)) thy
     1.5    in
     1.6      (pairself (pairself name_of) ((maybe_t, abs_t), (base_t, step_t)),
     1.7 -     Proof_Context.transfer_syntax thy ctxt)
     1.8 +     Proof_Context.transfer thy ctxt)
     1.9    end
    1.10  
    1.11  (** Term reconstruction **)
     2.1 --- a/src/Pure/Isar/proof_context.ML	Mon Feb 24 13:52:48 2014 +0100
     2.2 +++ b/src/Pure/Isar/proof_context.ML	Mon Feb 24 14:58:40 2014 +0100
     2.3 @@ -50,7 +50,6 @@
     2.4    val extern_const: Proof.context -> string -> xstring
     2.5    val markup_const: Proof.context -> string -> string
     2.6    val pretty_const: Proof.context -> string -> Pretty.T
     2.7 -  val transfer_syntax: theory -> Proof.context -> Proof.context
     2.8    val transfer: theory -> Proof.context -> Proof.context
     2.9    val background_theory: (theory -> theory) -> Proof.context -> Proof.context
    2.10    val background_theory_result: (theory -> 'a * theory) -> Proof.context -> 'a * Proof.context
     3.1 --- a/src/Pure/Proof/proof_syntax.ML	Mon Feb 24 13:52:48 2014 +0100
     3.2 +++ b/src/Pure/Proof/proof_syntax.ML	Mon Feb 24 14:58:40 2014 +0100
     3.3 @@ -246,7 +246,7 @@
     3.4  
     3.5  fun pretty_proof ctxt prf =
     3.6    Proof_Context.pretty_term_abbrev
     3.7 -    (Proof_Context.transfer_syntax (proof_syntax prf (Proof_Context.theory_of ctxt)) ctxt)
     3.8 +    (Proof_Context.transfer (proof_syntax prf (Proof_Context.theory_of ctxt)) ctxt)
     3.9      (term_of_proof prf);
    3.10  
    3.11  fun pretty_proof_of ctxt full th =