prefer Proof.context over Context.generic;
authorwenzelm
Thu Nov 23 22:38:30 2006 +0100 (2006-11-23)
changeset 21506b2a673894ce5
parent 21505 13d4dba99337
child 21507 f67b41110edd
prefer Proof.context over Context.generic;
src/HOL/Hyperreal/transfer.ML
src/HOL/Tools/res_atp.ML
src/HOL/Tools/res_atpset.ML
src/Pure/Isar/calculation.ML
src/Pure/Isar/context_rules.ML
src/Pure/Isar/induct_attrib.ML
src/Pure/Isar/isar_cmd.ML
src/Pure/Isar/local_defs.ML
src/Pure/Isar/outer_syntax.ML
src/Pure/Isar/toplevel.ML
src/Pure/Tools/nbe.ML
src/Pure/codegen.ML
src/ZF/Tools/typechk.ML
     1.1 --- a/src/HOL/Hyperreal/transfer.ML	Thu Nov 23 22:38:29 2006 +0100
     1.2 +++ b/src/HOL/Hyperreal/transfer.ML	Thu Nov 23 22:38:30 2006 +0100
     1.3 @@ -60,7 +60,7 @@
     1.4    let
     1.5      val thy = ProofContext.theory_of ctxt;
     1.6      val {intros,unfolds,refolds,consts} = TransferData.get (Context.Proof ctxt)
     1.7 -    val meta = LocalDefs.meta_rewrite_rule (Context.Proof ctxt)
     1.8 +    val meta = LocalDefs.meta_rewrite_rule ctxt
     1.9      val unfolds' = map meta unfolds and refolds' = map meta refolds;
    1.10      val (_$_$t') = concl_of (Tactic.rewrite true unfolds' (cterm_of thy t))
    1.11      val u = unstar_term consts t'
     2.1 --- a/src/HOL/Tools/res_atp.ML	Thu Nov 23 22:38:29 2006 +0100
     2.2 +++ b/src/HOL/Tools/res_atp.ML	Thu Nov 23 22:38:30 2006 +0100
     2.3 @@ -581,13 +581,13 @@
     2.4  	          (name_thm_pairs ctxt))
     2.5  	else 
     2.6  	let val claset_thms =
     2.7 -		if !include_claset then ResAxioms.claset_rules_of_ctxt ctxt
     2.8 +		if !include_claset then ResAxioms.claset_rules_of ctxt
     2.9  		else []
    2.10  	    val simpset_thms = 
    2.11 -		if !include_simpset then ResAxioms.simpset_rules_of_ctxt ctxt
    2.12 +		if !include_simpset then ResAxioms.simpset_rules_of ctxt
    2.13  		else []
    2.14  	    val atpset_thms =
    2.15 -		if !include_atpset then ResAxioms.atpset_rules_of_ctxt ctxt
    2.16 +		if !include_atpset then ResAxioms.atpset_rules_of ctxt
    2.17  		else []
    2.18  	    val _ = if !Output.show_debug_msgs 
    2.19  		    then (Output.debug "ATP theorems: "; display_thms atpset_thms) 
     3.1 --- a/src/HOL/Tools/res_atpset.ML	Thu Nov 23 22:38:29 2006 +0100
     3.2 +++ b/src/HOL/Tools/res_atpset.ML	Thu Nov 23 22:38:30 2006 +0100
     3.3 @@ -6,8 +6,8 @@
     3.4  
     3.5  signature RES_ATPSET =
     3.6  sig
     3.7 -  val print_atpset: Context.generic -> unit
     3.8 -  val get_atpset: Context.generic -> thm list
     3.9 +  val print_atpset: Proof.context -> unit
    3.10 +  val get_atpset: Proof.context -> thm list
    3.11    val atp_add: attribute
    3.12    val atp_del: attribute
    3.13    val setup: theory -> theory
    3.14 @@ -28,8 +28,8 @@
    3.15        (map (ProofContext.pretty_thm (Context.proof_of context)) rules));
    3.16  );
    3.17  
    3.18 -val print_atpset = Data.print;
    3.19 -val get_atpset = Data.get;
    3.20 +val print_atpset = Data.print o Context.Proof;
    3.21 +val get_atpset = Data.get o Context.Proof;
    3.22  
    3.23  val atp_add = Thm.declaration_attribute (Data.map o Drule.add_rule);
    3.24  val atp_del = Thm.declaration_attribute (Data.map o Drule.del_rule);
     4.1 --- a/src/Pure/Isar/calculation.ML	Thu Nov 23 22:38:29 2006 +0100
     4.2 +++ b/src/Pure/Isar/calculation.ML	Thu Nov 23 22:38:30 2006 +0100
     4.3 @@ -7,7 +7,7 @@
     4.4  
     4.5  signature CALCULATION =
     4.6  sig
     4.7 -  val print_rules: Context.generic -> unit
     4.8 +  val print_rules: Proof.context -> unit
     4.9    val get_calculation: Proof.state -> thm list option
    4.10    val trans_add: attribute
    4.11    val trans_del: attribute
    4.12 @@ -47,7 +47,7 @@
    4.13  );
    4.14  
    4.15  val _ = Context.add_setup CalculationData.init;
    4.16 -val print_rules = CalculationData.print;
    4.17 +val print_rules = CalculationData.print o Context.Proof;
    4.18  
    4.19  
    4.20  (* access calculation *)
     5.1 --- a/src/Pure/Isar/context_rules.ML	Thu Nov 23 22:38:29 2006 +0100
     5.2 +++ b/src/Pure/Isar/context_rules.ML	Thu Nov 23 22:38:30 2006 +0100
     5.3 @@ -15,7 +15,7 @@
     5.4    val orderlist: ((int * int) * 'a) list -> 'a list
     5.5    val find_rules_netpair: bool -> thm list -> term -> netpair -> thm list
     5.6    val find_rules: bool -> thm list -> term -> Proof.context -> thm list list
     5.7 -  val print_rules: Context.generic -> unit
     5.8 +  val print_rules: Proof.context -> unit
     5.9    val addSWrapper: ((int -> tactic) -> int -> tactic) -> theory -> theory
    5.10    val addWrapper: ((int -> tactic) -> int -> tactic) -> theory -> theory
    5.11    val Swrap: Proof.context -> (int -> tactic) -> int -> tactic
    5.12 @@ -125,7 +125,7 @@
    5.13  );
    5.14  
    5.15  val _ = Context.add_setup Rules.init;
    5.16 -val print_rules = Rules.print;
    5.17 +val print_rules = Rules.print o Context.Proof;
    5.18  
    5.19  
    5.20  (* access data *)
     6.1 --- a/src/Pure/Isar/induct_attrib.ML	Thu Nov 23 22:38:29 2006 +0100
     6.2 +++ b/src/Pure/Isar/induct_attrib.ML	Thu Nov 23 22:38:30 2006 +0100
     6.3 @@ -8,11 +8,11 @@
     6.4  signature INDUCT_ATTRIB =
     6.5  sig
     6.6    val vars_of: term -> term list
     6.7 -  val dest_rules: Context.generic ->
     6.8 +  val dest_rules: Proof.context ->
     6.9      {type_cases: (string * thm) list, set_cases: (string * thm) list,
    6.10        type_induct: (string * thm) list, set_induct: (string * thm) list,
    6.11        type_coinduct: (string * thm) list, set_coinduct: (string * thm) list}
    6.12 -  val print_rules: Context.generic -> unit
    6.13 +  val print_rules: Proof.context -> unit
    6.14    val lookup_casesT : Proof.context -> string -> thm option
    6.15    val lookup_casesS : Proof.context -> string -> thm option
    6.16    val lookup_inductT : Proof.context -> string -> thm option
    6.17 @@ -133,8 +133,8 @@
    6.18  );
    6.19  
    6.20  val _ = Context.add_setup Induct.init;
    6.21 -val print_rules = Induct.print;
    6.22 -val dest_rules = dest o Induct.get;
    6.23 +val print_rules = Induct.print o Context.Proof;
    6.24 +val dest_rules = dest o Induct.get o Context.Proof;
    6.25  
    6.26  val get_local = Induct.get o Context.Proof;
    6.27  
     7.1 --- a/src/Pure/Isar/isar_cmd.ML	Thu Nov 23 22:38:29 2006 +0100
     7.2 +++ b/src/Pure/Isar/isar_cmd.ML	Thu Nov 23 22:38:30 2006 +0100
     7.3 @@ -339,7 +339,7 @@
     7.4  
     7.5  val print_facts = Toplevel.unknown_context o Toplevel.keep (fn state =>
     7.6    ProofContext.setmp_verbose
     7.7 -    ProofContext.print_lthms (Context.proof_of (Toplevel.context_of state)));
     7.8 +    ProofContext.print_lthms (Toplevel.context_of state));
     7.9  
    7.10  val print_theorems_proof = Toplevel.keep (fn state =>
    7.11    ProofContext.setmp_verbose
     8.1 --- a/src/Pure/Isar/local_defs.ML	Thu Nov 23 22:38:29 2006 +0100
     8.2 +++ b/src/Pure/Isar/local_defs.ML	Thu Nov 23 22:38:30 2006 +0100
     8.3 @@ -14,10 +14,10 @@
     8.4    val find_def: Proof.context -> string -> thm option
     8.5    val add_defs: ((string * mixfix) * ((bstring * attribute list) * term)) list -> Proof.context ->
     8.6      (term * (bstring * thm)) list * Proof.context
     8.7 -  val print_rules: Context.generic -> unit
     8.8 +  val print_rules: Proof.context -> unit
     8.9    val defn_add: attribute
    8.10    val defn_del: attribute
    8.11 -  val meta_rewrite_rule: Context.generic -> thm -> thm
    8.12 +  val meta_rewrite_rule: Proof.context -> thm -> thm
    8.13    val unfold: Proof.context -> thm list -> thm -> thm
    8.14    val unfold_goals: Proof.context -> thm list -> thm -> thm
    8.15    val unfold_tac: Proof.context -> thm list -> tactic
    8.16 @@ -122,7 +122,7 @@
    8.17  
    8.18  val _ = Context.add_setup Rules.init;
    8.19  
    8.20 -val print_rules = Rules.print;
    8.21 +val print_rules = Rules.print o Context.Proof;
    8.22  
    8.23  val defn_add = Thm.declaration_attribute (Rules.map o Drule.add_rule);
    8.24  val defn_del = Thm.declaration_attribute (Rules.map o Drule.del_rule);
    8.25 @@ -134,19 +134,19 @@
    8.26    MetaSimplifier.theory_context ProtoPure.thy MetaSimplifier.empty_ss
    8.27      addeqcongs [Drule.equals_cong];    (*protect meta-level equality*)
    8.28  
    8.29 -fun meta_rewrite context =
    8.30 +fun meta_rewrite ctxt =
    8.31    MetaSimplifier.rewrite_cterm (false, false, false) (K (K NONE))
    8.32 -    (equals_ss addsimps (Rules.get context));
    8.33 +    (equals_ss addsimps (Rules.get (Context.Proof ctxt)));
    8.34  
    8.35  val meta_rewrite_rule = Drule.fconv_rule o meta_rewrite;
    8.36  
    8.37  fun meta_rewrite_tac ctxt i =
    8.38 -  PRIMITIVE (Drule.fconv_rule (Drule.goals_conv (equal i) (meta_rewrite (Context.Proof ctxt))));
    8.39 +  PRIMITIVE (Drule.fconv_rule (Drule.goals_conv (equal i) (meta_rewrite ctxt)));
    8.40  
    8.41  
    8.42  (* rewriting with object-level rules *)
    8.43  
    8.44 -fun meta f ctxt = f o map (meta_rewrite_rule (Context.Proof ctxt));
    8.45 +fun meta f ctxt = f o map (meta_rewrite_rule ctxt);
    8.46  
    8.47  val unfold       = meta Tactic.rewrite_rule;
    8.48  val unfold_goals = meta Tactic.rewrite_goals_rule;
    8.49 @@ -161,7 +161,7 @@
    8.50    let
    8.51      val ((c, T), rhs) = prop
    8.52        |> Thm.cterm_of (ProofContext.theory_of ctxt)
    8.53 -      |> meta_rewrite (Context.Proof ctxt)
    8.54 +      |> meta_rewrite ctxt
    8.55        |> (snd o Logic.dest_equals o Thm.prop_of)
    8.56        |> K conditional ? Logic.strip_imp_concl
    8.57        |> (abs_def o #2 o cert_def ctxt);
     9.1 --- a/src/Pure/Isar/outer_syntax.ML	Thu Nov 23 22:38:29 2006 +0100
     9.2 +++ b/src/Pure/Isar/outer_syntax.ML	Thu Nov 23 22:38:30 2006 +0100
     9.3 @@ -328,7 +328,7 @@
     9.4    val exn = Toplevel.exn;
     9.5  
     9.6    fun context () =
     9.7 -    Context.proof_of (Toplevel.context_of (state ()))
     9.8 +    Toplevel.context_of (state ())
     9.9        handle Toplevel.UNDEF => error "Unknown context";
    9.10  
    9.11    fun goal () =
    10.1 --- a/src/Pure/Isar/toplevel.ML	Thu Nov 23 22:38:29 2006 +0100
    10.2 +++ b/src/Pure/Isar/toplevel.ML	Thu Nov 23 22:38:30 2006 +0100
    10.3 @@ -24,7 +24,7 @@
    10.4    val node_history_of: state -> node History.T
    10.5    val node_of: state -> node
    10.6    val node_case: (generic_theory -> 'a) -> (Proof.state -> 'a) -> state -> 'a
    10.7 -  val context_of: state -> Context.generic
    10.8 +  val context_of: state -> Proof.context
    10.9    val theory_of: state -> theory
   10.10    val proof_of: state -> Proof.state
   10.11    val proof_position_of: state -> int
   10.12 @@ -189,7 +189,7 @@
   10.13  
   10.14  fun node_case f g state = cases_node f g (node_of state);
   10.15  
   10.16 -val context_of = node_case I (Context.Proof o Proof.context_of);
   10.17 +val context_of = node_case Context.proof_of Proof.context_of;
   10.18  val theory_of = node_case Context.theory_of Proof.theory_of;
   10.19  val proof_of = node_case (fn _ => raise UNDEF) I;
   10.20  
   10.21 @@ -214,7 +214,8 @@
   10.22  val pretty_context = LocalTheory.pretty o Context.cases (loc_init NONE) I;
   10.23  
   10.24  fun pretty_state_context state =
   10.25 -  (case try context_of state of NONE => []
   10.26 +  (case try (node_case I (Context.Proof o Proof.context_of)) state of
   10.27 +    NONE => []
   10.28    | SOME gthy => pretty_context gthy);
   10.29  
   10.30  fun pretty_node prf_only (Theory (gthy, _)) = if prf_only then [] else pretty_context gthy
    11.1 --- a/src/Pure/Tools/nbe.ML	Thu Nov 23 22:38:29 2006 +0100
    11.2 +++ b/src/Pure/Tools/nbe.ML	Thu Nov 23 22:38:30 2006 +0100
    11.3 @@ -59,9 +59,9 @@
    11.4  
    11.5  fun consts_of_pres thy = 
    11.6    let
    11.7 +    val ctxt = ProofContext.init thy;
    11.8      val pres = fst (NBE_Rewrite.get thy);
    11.9 -    val rhss = map (snd o Logic.dest_equals o prop_of
   11.10 -      o LocalDefs.meta_rewrite_rule (Context.Theory thy)) pres;
   11.11 +    val rhss = map (snd o Logic.dest_equals o prop_of o LocalDefs.meta_rewrite_rule ctxt) pres;
   11.12    in
   11.13      (fold o fold_aterms)
   11.14        (fn Const c => insert (op =) (CodegenConsts.norm_of_typ thy c) | _ => I)
   11.15 @@ -70,14 +70,14 @@
   11.16  
   11.17  fun apply_pres thy =
   11.18    let
   11.19 -    val pres =
   11.20 -      (map (LocalDefs.meta_rewrite_rule (Context.Theory thy)) o fst) (NBE_Rewrite.get thy)
   11.21 +    val ctxt = ProofContext.init thy;
   11.22 +    val pres = (map (LocalDefs.meta_rewrite_rule ctxt) o fst) (NBE_Rewrite.get thy)
   11.23    in map (CodegenData.rewrite_func pres) end
   11.24  
   11.25  fun apply_posts thy =
   11.26    let
   11.27 -    val posts =
   11.28 -      (map (LocalDefs.meta_rewrite_rule (Context.Theory thy)) o snd) (NBE_Rewrite.get thy)
   11.29 +    val ctxt = ProofContext.init thy;
   11.30 +    val posts = (map (LocalDefs.meta_rewrite_rule ctxt) o snd) (NBE_Rewrite.get thy)
   11.31    in Tactic.rewrite false posts end
   11.32  
   11.33  
   11.34 @@ -213,8 +213,7 @@
   11.35    in Pretty.writeln p end;
   11.36  
   11.37  fun norm_print_term_e (modes, raw_t) state =
   11.38 -  let
   11.39 -    val ctxt = Context.proof_of (Toplevel.context_of state);
   11.40 +  let val ctxt = Toplevel.context_of state
   11.41    in norm_print_term ctxt modes (ProofContext.read_term ctxt raw_t) end;
   11.42  
   11.43  val _ = Context.add_setup
    12.1 --- a/src/Pure/codegen.ML	Thu Nov 23 22:38:29 2006 +0100
    12.2 +++ b/src/Pure/codegen.ML	Thu Nov 23 22:38:30 2006 +0100
    12.3 @@ -1048,7 +1048,7 @@
    12.4  
    12.5  fun print_evaluated_term s = Toplevel.keep (fn state =>
    12.6    let
    12.7 -    val ctxt = Context.proof_of (Toplevel.context_of state);
    12.8 +    val ctxt = Toplevel.context_of state;
    12.9      val thy = ProofContext.theory_of ctxt;
   12.10      val t = eval_term thy (ProofContext.read_term ctxt s);
   12.11      val T = Term.type_of t;
    13.1 --- a/src/ZF/Tools/typechk.ML	Thu Nov 23 22:38:29 2006 +0100
    13.2 +++ b/src/ZF/Tools/typechk.ML	Thu Nov 23 22:38:30 2006 +0100
    13.3 @@ -8,7 +8,7 @@
    13.4  
    13.5  signature TYPE_CHECK =
    13.6  sig
    13.7 -  val print_tcset: Context.generic -> unit
    13.8 +  val print_tcset: Proof.context -> unit
    13.9    val TC_add: attribute
   13.10    val TC_del: attribute
   13.11    val typecheck_tac: Proof.context -> tactic
   13.12 @@ -58,7 +58,7 @@
   13.13        (map (ProofContext.pretty_thm (Context.proof_of context)) rules));
   13.14  );
   13.15  
   13.16 -val print_tcset = Data.print;
   13.17 +val print_tcset = Data.print o Context.Proof;
   13.18  
   13.19  val TC_add = Thm.declaration_attribute (Data.map o add_rule);
   13.20  val TC_del = Thm.declaration_attribute (Data.map o del_rule);