# HG changeset patch # User wenzelm # Date 1164317910 -3600 # Node ID b2a673894ce521de6d0713dd941f57a601cbe29b # Parent 13d4dba9933732f575ab192c740c6426932bfa14 prefer Proof.context over Context.generic; diff -r 13d4dba99337 -r b2a673894ce5 src/HOL/Hyperreal/transfer.ML --- a/src/HOL/Hyperreal/transfer.ML Thu Nov 23 22:38:29 2006 +0100 +++ b/src/HOL/Hyperreal/transfer.ML Thu Nov 23 22:38:30 2006 +0100 @@ -60,7 +60,7 @@ let val thy = ProofContext.theory_of ctxt; val {intros,unfolds,refolds,consts} = TransferData.get (Context.Proof ctxt) - val meta = LocalDefs.meta_rewrite_rule (Context.Proof ctxt) + val meta = LocalDefs.meta_rewrite_rule ctxt val unfolds' = map meta unfolds and refolds' = map meta refolds; val (_$_$t') = concl_of (Tactic.rewrite true unfolds' (cterm_of thy t)) val u = unstar_term consts t' diff -r 13d4dba99337 -r b2a673894ce5 src/HOL/Tools/res_atp.ML --- a/src/HOL/Tools/res_atp.ML Thu Nov 23 22:38:29 2006 +0100 +++ b/src/HOL/Tools/res_atp.ML Thu Nov 23 22:38:30 2006 +0100 @@ -581,13 +581,13 @@ (name_thm_pairs ctxt)) else let val claset_thms = - if !include_claset then ResAxioms.claset_rules_of_ctxt ctxt + if !include_claset then ResAxioms.claset_rules_of ctxt else [] val simpset_thms = - if !include_simpset then ResAxioms.simpset_rules_of_ctxt ctxt + if !include_simpset then ResAxioms.simpset_rules_of ctxt else [] val atpset_thms = - if !include_atpset then ResAxioms.atpset_rules_of_ctxt ctxt + if !include_atpset then ResAxioms.atpset_rules_of ctxt else [] val _ = if !Output.show_debug_msgs then (Output.debug "ATP theorems: "; display_thms atpset_thms) diff -r 13d4dba99337 -r b2a673894ce5 src/HOL/Tools/res_atpset.ML --- a/src/HOL/Tools/res_atpset.ML Thu Nov 23 22:38:29 2006 +0100 +++ b/src/HOL/Tools/res_atpset.ML Thu Nov 23 22:38:30 2006 +0100 @@ -6,8 +6,8 @@ signature RES_ATPSET = sig - val print_atpset: Context.generic -> unit - val get_atpset: Context.generic -> thm list + val print_atpset: Proof.context -> unit + val get_atpset: Proof.context -> thm list val atp_add: attribute val atp_del: attribute val setup: theory -> theory @@ -28,8 +28,8 @@ (map (ProofContext.pretty_thm (Context.proof_of context)) rules)); ); -val print_atpset = Data.print; -val get_atpset = Data.get; +val print_atpset = Data.print o Context.Proof; +val get_atpset = Data.get o Context.Proof; val atp_add = Thm.declaration_attribute (Data.map o Drule.add_rule); val atp_del = Thm.declaration_attribute (Data.map o Drule.del_rule); diff -r 13d4dba99337 -r b2a673894ce5 src/Pure/Isar/calculation.ML --- a/src/Pure/Isar/calculation.ML Thu Nov 23 22:38:29 2006 +0100 +++ b/src/Pure/Isar/calculation.ML Thu Nov 23 22:38:30 2006 +0100 @@ -7,7 +7,7 @@ signature CALCULATION = sig - val print_rules: Context.generic -> unit + val print_rules: Proof.context -> unit val get_calculation: Proof.state -> thm list option val trans_add: attribute val trans_del: attribute @@ -47,7 +47,7 @@ ); val _ = Context.add_setup CalculationData.init; -val print_rules = CalculationData.print; +val print_rules = CalculationData.print o Context.Proof; (* access calculation *) diff -r 13d4dba99337 -r b2a673894ce5 src/Pure/Isar/context_rules.ML --- a/src/Pure/Isar/context_rules.ML Thu Nov 23 22:38:29 2006 +0100 +++ b/src/Pure/Isar/context_rules.ML Thu Nov 23 22:38:30 2006 +0100 @@ -15,7 +15,7 @@ val orderlist: ((int * int) * 'a) list -> 'a list val find_rules_netpair: bool -> thm list -> term -> netpair -> thm list val find_rules: bool -> thm list -> term -> Proof.context -> thm list list - val print_rules: Context.generic -> unit + val print_rules: Proof.context -> unit val addSWrapper: ((int -> tactic) -> int -> tactic) -> theory -> theory val addWrapper: ((int -> tactic) -> int -> tactic) -> theory -> theory val Swrap: Proof.context -> (int -> tactic) -> int -> tactic @@ -125,7 +125,7 @@ ); val _ = Context.add_setup Rules.init; -val print_rules = Rules.print; +val print_rules = Rules.print o Context.Proof; (* access data *) diff -r 13d4dba99337 -r b2a673894ce5 src/Pure/Isar/induct_attrib.ML --- a/src/Pure/Isar/induct_attrib.ML Thu Nov 23 22:38:29 2006 +0100 +++ b/src/Pure/Isar/induct_attrib.ML Thu Nov 23 22:38:30 2006 +0100 @@ -8,11 +8,11 @@ signature INDUCT_ATTRIB = sig val vars_of: term -> term list - val dest_rules: Context.generic -> + val dest_rules: Proof.context -> {type_cases: (string * thm) list, set_cases: (string * thm) list, type_induct: (string * thm) list, set_induct: (string * thm) list, type_coinduct: (string * thm) list, set_coinduct: (string * thm) list} - val print_rules: Context.generic -> unit + val print_rules: Proof.context -> unit val lookup_casesT : Proof.context -> string -> thm option val lookup_casesS : Proof.context -> string -> thm option val lookup_inductT : Proof.context -> string -> thm option @@ -133,8 +133,8 @@ ); val _ = Context.add_setup Induct.init; -val print_rules = Induct.print; -val dest_rules = dest o Induct.get; +val print_rules = Induct.print o Context.Proof; +val dest_rules = dest o Induct.get o Context.Proof; val get_local = Induct.get o Context.Proof; diff -r 13d4dba99337 -r b2a673894ce5 src/Pure/Isar/isar_cmd.ML --- a/src/Pure/Isar/isar_cmd.ML Thu Nov 23 22:38:29 2006 +0100 +++ b/src/Pure/Isar/isar_cmd.ML Thu Nov 23 22:38:30 2006 +0100 @@ -339,7 +339,7 @@ val print_facts = Toplevel.unknown_context o Toplevel.keep (fn state => ProofContext.setmp_verbose - ProofContext.print_lthms (Context.proof_of (Toplevel.context_of state))); + ProofContext.print_lthms (Toplevel.context_of state)); val print_theorems_proof = Toplevel.keep (fn state => ProofContext.setmp_verbose diff -r 13d4dba99337 -r b2a673894ce5 src/Pure/Isar/local_defs.ML --- a/src/Pure/Isar/local_defs.ML Thu Nov 23 22:38:29 2006 +0100 +++ b/src/Pure/Isar/local_defs.ML Thu Nov 23 22:38:30 2006 +0100 @@ -14,10 +14,10 @@ val find_def: Proof.context -> string -> thm option val add_defs: ((string * mixfix) * ((bstring * attribute list) * term)) list -> Proof.context -> (term * (bstring * thm)) list * Proof.context - val print_rules: Context.generic -> unit + val print_rules: Proof.context -> unit val defn_add: attribute val defn_del: attribute - val meta_rewrite_rule: Context.generic -> thm -> thm + val meta_rewrite_rule: Proof.context -> thm -> thm val unfold: Proof.context -> thm list -> thm -> thm val unfold_goals: Proof.context -> thm list -> thm -> thm val unfold_tac: Proof.context -> thm list -> tactic @@ -122,7 +122,7 @@ val _ = Context.add_setup Rules.init; -val print_rules = Rules.print; +val print_rules = Rules.print o Context.Proof; val defn_add = Thm.declaration_attribute (Rules.map o Drule.add_rule); val defn_del = Thm.declaration_attribute (Rules.map o Drule.del_rule); @@ -134,19 +134,19 @@ MetaSimplifier.theory_context ProtoPure.thy MetaSimplifier.empty_ss addeqcongs [Drule.equals_cong]; (*protect meta-level equality*) -fun meta_rewrite context = +fun meta_rewrite ctxt = MetaSimplifier.rewrite_cterm (false, false, false) (K (K NONE)) - (equals_ss addsimps (Rules.get context)); + (equals_ss addsimps (Rules.get (Context.Proof ctxt))); val meta_rewrite_rule = Drule.fconv_rule o meta_rewrite; fun meta_rewrite_tac ctxt i = - PRIMITIVE (Drule.fconv_rule (Drule.goals_conv (equal i) (meta_rewrite (Context.Proof ctxt)))); + PRIMITIVE (Drule.fconv_rule (Drule.goals_conv (equal i) (meta_rewrite ctxt))); (* rewriting with object-level rules *) -fun meta f ctxt = f o map (meta_rewrite_rule (Context.Proof ctxt)); +fun meta f ctxt = f o map (meta_rewrite_rule ctxt); val unfold = meta Tactic.rewrite_rule; val unfold_goals = meta Tactic.rewrite_goals_rule; @@ -161,7 +161,7 @@ let val ((c, T), rhs) = prop |> Thm.cterm_of (ProofContext.theory_of ctxt) - |> meta_rewrite (Context.Proof ctxt) + |> meta_rewrite ctxt |> (snd o Logic.dest_equals o Thm.prop_of) |> K conditional ? Logic.strip_imp_concl |> (abs_def o #2 o cert_def ctxt); diff -r 13d4dba99337 -r b2a673894ce5 src/Pure/Isar/outer_syntax.ML --- a/src/Pure/Isar/outer_syntax.ML Thu Nov 23 22:38:29 2006 +0100 +++ b/src/Pure/Isar/outer_syntax.ML Thu Nov 23 22:38:30 2006 +0100 @@ -328,7 +328,7 @@ val exn = Toplevel.exn; fun context () = - Context.proof_of (Toplevel.context_of (state ())) + Toplevel.context_of (state ()) handle Toplevel.UNDEF => error "Unknown context"; fun goal () = diff -r 13d4dba99337 -r b2a673894ce5 src/Pure/Isar/toplevel.ML --- a/src/Pure/Isar/toplevel.ML Thu Nov 23 22:38:29 2006 +0100 +++ b/src/Pure/Isar/toplevel.ML Thu Nov 23 22:38:30 2006 +0100 @@ -24,7 +24,7 @@ val node_history_of: state -> node History.T val node_of: state -> node val node_case: (generic_theory -> 'a) -> (Proof.state -> 'a) -> state -> 'a - val context_of: state -> Context.generic + val context_of: state -> Proof.context val theory_of: state -> theory val proof_of: state -> Proof.state val proof_position_of: state -> int @@ -189,7 +189,7 @@ fun node_case f g state = cases_node f g (node_of state); -val context_of = node_case I (Context.Proof o Proof.context_of); +val context_of = node_case Context.proof_of Proof.context_of; val theory_of = node_case Context.theory_of Proof.theory_of; val proof_of = node_case (fn _ => raise UNDEF) I; @@ -214,7 +214,8 @@ val pretty_context = LocalTheory.pretty o Context.cases (loc_init NONE) I; fun pretty_state_context state = - (case try context_of state of NONE => [] + (case try (node_case I (Context.Proof o Proof.context_of)) state of + NONE => [] | SOME gthy => pretty_context gthy); fun pretty_node prf_only (Theory (gthy, _)) = if prf_only then [] else pretty_context gthy diff -r 13d4dba99337 -r b2a673894ce5 src/Pure/Tools/nbe.ML --- a/src/Pure/Tools/nbe.ML Thu Nov 23 22:38:29 2006 +0100 +++ b/src/Pure/Tools/nbe.ML Thu Nov 23 22:38:30 2006 +0100 @@ -59,9 +59,9 @@ fun consts_of_pres thy = let + val ctxt = ProofContext.init thy; val pres = fst (NBE_Rewrite.get thy); - val rhss = map (snd o Logic.dest_equals o prop_of - o LocalDefs.meta_rewrite_rule (Context.Theory thy)) pres; + val rhss = map (snd o Logic.dest_equals o prop_of o LocalDefs.meta_rewrite_rule ctxt) pres; in (fold o fold_aterms) (fn Const c => insert (op =) (CodegenConsts.norm_of_typ thy c) | _ => I) @@ -70,14 +70,14 @@ fun apply_pres thy = let - val pres = - (map (LocalDefs.meta_rewrite_rule (Context.Theory thy)) o fst) (NBE_Rewrite.get thy) + val ctxt = ProofContext.init thy; + val pres = (map (LocalDefs.meta_rewrite_rule ctxt) o fst) (NBE_Rewrite.get thy) in map (CodegenData.rewrite_func pres) end fun apply_posts thy = let - val posts = - (map (LocalDefs.meta_rewrite_rule (Context.Theory thy)) o snd) (NBE_Rewrite.get thy) + val ctxt = ProofContext.init thy; + val posts = (map (LocalDefs.meta_rewrite_rule ctxt) o snd) (NBE_Rewrite.get thy) in Tactic.rewrite false posts end @@ -213,8 +213,7 @@ in Pretty.writeln p end; fun norm_print_term_e (modes, raw_t) state = - let - val ctxt = Context.proof_of (Toplevel.context_of state); + let val ctxt = Toplevel.context_of state in norm_print_term ctxt modes (ProofContext.read_term ctxt raw_t) end; val _ = Context.add_setup diff -r 13d4dba99337 -r b2a673894ce5 src/Pure/codegen.ML --- a/src/Pure/codegen.ML Thu Nov 23 22:38:29 2006 +0100 +++ b/src/Pure/codegen.ML Thu Nov 23 22:38:30 2006 +0100 @@ -1048,7 +1048,7 @@ fun print_evaluated_term s = Toplevel.keep (fn state => let - val ctxt = Context.proof_of (Toplevel.context_of state); + val ctxt = Toplevel.context_of state; val thy = ProofContext.theory_of ctxt; val t = eval_term thy (ProofContext.read_term ctxt s); val T = Term.type_of t; diff -r 13d4dba99337 -r b2a673894ce5 src/ZF/Tools/typechk.ML --- a/src/ZF/Tools/typechk.ML Thu Nov 23 22:38:29 2006 +0100 +++ b/src/ZF/Tools/typechk.ML Thu Nov 23 22:38:30 2006 +0100 @@ -8,7 +8,7 @@ signature TYPE_CHECK = sig - val print_tcset: Context.generic -> unit + val print_tcset: Proof.context -> unit val TC_add: attribute val TC_del: attribute val typecheck_tac: Proof.context -> tactic @@ -58,7 +58,7 @@ (map (ProofContext.pretty_thm (Context.proof_of context)) rules)); ); -val print_tcset = Data.print; +val print_tcset = Data.print o Context.Proof; val TC_add = Thm.declaration_attribute (Data.map o add_rule); val TC_del = Thm.declaration_attribute (Data.map o del_rule);