src/HOL/Tools/Nitpick/nitpick_model.ML
changeset 42361 23f352990944
parent 41993 bd6296de1432
child 42375 774df7c59508
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick_model.ML	Sat Apr 16 15:47:52 2011 +0200
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_model.ML	Sat Apr 16 16:15:37 2011 +0200
     1.3 @@ -94,7 +94,7 @@
     1.4  fun add_wacky_syntax ctxt =
     1.5    let
     1.6      val name_of = fst o dest_Const
     1.7 -    val thy = ProofContext.theory_of ctxt |> Context.reject_draft
     1.8 +    val thy = Proof_Context.theory_of ctxt |> Context.reject_draft
     1.9      val (maybe_t, thy) =
    1.10        Sign.declare_const ((@{binding nitpick_maybe}, @{typ "'a => 'a"}),
    1.11                            Mixfix (maybe_mixfix (), [1000], 1000)) thy
    1.12 @@ -109,7 +109,7 @@
    1.13                            Mixfix (step_mixfix (), [1000], 1000)) thy
    1.14    in
    1.15      (pairself (pairself name_of) ((maybe_t, abs_t), (base_t, step_t)),
    1.16 -     ProofContext.transfer_syntax thy ctxt)
    1.17 +     Proof_Context.transfer_syntax thy ctxt)
    1.18    end
    1.19  
    1.20  (** Term reconstruction **)
    1.21 @@ -329,7 +329,7 @@
    1.22    | mk_tuple T [] = raise TYPE ("Nitpick_Model.mk_tuple", [T], [])
    1.23  
    1.24  fun varified_type_match ctxt (candid_T, pat_T) =
    1.25 -  let val thy = ProofContext.theory_of ctxt in
    1.26 +  let val thy = Proof_Context.theory_of ctxt in
    1.27      strict_type_match thy (candid_T, varify_type ctxt pat_T)
    1.28    end
    1.29