# 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);