--- 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'
--- 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)
--- 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);
--- 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 *)
--- 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 *)
--- 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;
--- 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
--- 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);
--- 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 () =
--- 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
--- 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
--- 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;
--- 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);