discontinued obsolete alias structure ProofContext;
authorwenzelm
Wed Oct 12 16:21:07 2011 +0200 (2011-10-12 ago)
changeset 451285af3a3203a76
parent 45127 d2eb07a1e01b
child 45129 1fce03e3e8ad
discontinued obsolete alias structure ProofContext;
NEWS
src/HOL/Nitpick_Examples/minipick.ML
src/Pure/pure_setup.ML
src/Tools/Code/code_thingol.ML
     1.1 --- a/NEWS	Wed Oct 12 09:16:30 2011 +0200
     1.2 +++ b/NEWS	Wed Oct 12 16:21:07 2011 +0200
     1.3 @@ -44,6 +44,12 @@
     1.4    zero_le_zpower_abs ~> zero_le_power_abs
     1.5  
     1.6  
     1.7 +*** ML ***
     1.8 +
     1.9 +* Structure Proof_Context follows standard naming scheme.  Old
    1.10 +ProofContext has been discontinued.  INCOMPATIBILITY.
    1.11 +
    1.12 +
    1.13  
    1.14  New in Isabelle2011-1 (October 2011)
    1.15  ------------------------------------
     2.1 --- a/src/HOL/Nitpick_Examples/minipick.ML	Wed Oct 12 09:16:30 2011 +0200
     2.2 +++ b/src/HOL/Nitpick_Examples/minipick.ML	Wed Oct 12 16:21:07 2011 +0200
     2.3 @@ -381,7 +381,7 @@
     2.4  
     2.5  fun kodkod_problem_from_term ctxt total raw_card raw_infinite t =
     2.6    let
     2.7 -    val thy = ProofContext.theory_of ctxt
     2.8 +    val thy = Proof_Context.theory_of ctxt
     2.9      fun card (Type (@{type_name fun}, [T1, T2])) =
    2.10          reasonable_power (card T2) (card T1)
    2.11        | card (Type (@{type_name prod}, [T1, T2])) = card T1 * card T2
    2.12 @@ -433,7 +433,7 @@
    2.13  
    2.14  fun minipick ctxt n t =
    2.15    let
    2.16 -    val thy = ProofContext.theory_of ctxt
    2.17 +    val thy = Proof_Context.theory_of ctxt
    2.18      val {total_consts, ...} = Nitpick_Isar.default_params thy []
    2.19      val totals =
    2.20        total_consts |> Option.map single |> the_default [true, false]
     3.1 --- a/src/Pure/pure_setup.ML	Wed Oct 12 09:16:30 2011 +0200
     3.2 +++ b/src/Pure/pure_setup.ML	Wed Oct 12 16:21:07 2011 +0200
     3.3 @@ -57,6 +57,3 @@
     3.4  
     3.5  Proofterm.proofs := 0;
     3.6  
     3.7 -(*legacy*)
     3.8 -structure ProofContext = Proof_Context;
     3.9 -
     4.1 --- a/src/Tools/Code/code_thingol.ML	Wed Oct 12 09:16:30 2011 +0200
     4.2 +++ b/src/Tools/Code/code_thingol.ML	Wed Oct 12 16:21:07 2011 +0200
     4.3 @@ -606,7 +606,7 @@
     4.4  
     4.5  fun annotate thy algbr eqngr (c, ty) args rhs =
     4.6    let
     4.7 -    val ctxt = ProofContext.init_global thy |> Config.put Type_Infer_Context.const_sorts false
     4.8 +    val ctxt = Proof_Context.init_global thy |> Config.put Type_Infer_Context.const_sorts false
     4.9      val erase = map_types (fn _ => Type_Infer.anyT [])
    4.10      val reinfer = singleton (Type_Infer_Context.infer_types ctxt)
    4.11      val lhs = list_comb (Const (c, ty), map (map_types Type.strip_sorts o fst) args)