# HG changeset patch
# User wenzelm
# Date 1154550401 -7200
# Node ID ba7a7c56bed5a240dcd0a27b4d3fc4a25504f4bf
# Parent  8ff4a0ea49b210fcdaf3173d7951e221289f42f4
normalized Proof.context/method type aliases;

diff -r 8ff4a0ea49b2 -r ba7a7c56bed5 src/HOL/Nominal/nominal_permeq.ML
--- a/src/HOL/Nominal/nominal_permeq.ML	Wed Aug 02 22:26:40 2006 +0200
+++ b/src/HOL/Nominal/nominal_permeq.ML	Wed Aug 02 22:26:41 2006 +0200
@@ -14,16 +14,16 @@
   val finite_guess_tac : simpset -> int -> tactic
   val fresh_guess_tac : simpset -> int -> tactic
 
-  val perm_eq_meth : Method.src -> ProofContext.context -> Method.method
-  val perm_eq_meth_debug : Method.src -> ProofContext.context -> Method.method
-  val perm_full_eq_meth : Method.src -> ProofContext.context -> Method.method
-  val perm_full_eq_meth_debug : Method.src -> ProofContext.context -> Method.method
-  val supports_meth : Method.src -> ProofContext.context -> Method.method
-  val supports_meth_debug : Method.src -> ProofContext.context -> Method.method
-  val finite_gs_meth : Method.src -> ProofContext.context -> Method.method
-  val finite_gs_meth_debug : Method.src -> ProofContext.context -> Method.method
-  val fresh_gs_meth : Method.src -> ProofContext.context -> Method.method
-  val fresh_gs_meth_debug : Method.src -> ProofContext.context -> Method.method
+  val perm_eq_meth : Method.src -> Proof.context -> Proof.method
+  val perm_eq_meth_debug : Method.src -> Proof.context -> Proof.method
+  val perm_full_eq_meth : Method.src -> Proof.context -> Proof.method
+  val perm_full_eq_meth_debug : Method.src -> Proof.context -> Proof.method
+  val supports_meth : Method.src -> Proof.context -> Proof.method
+  val supports_meth_debug : Method.src -> Proof.context -> Proof.method
+  val finite_gs_meth : Method.src -> Proof.context -> Proof.method
+  val finite_gs_meth_debug : Method.src -> Proof.context -> Proof.method
+  val fresh_gs_meth : Method.src -> Proof.context -> Proof.method
+  val fresh_gs_meth_debug : Method.src -> Proof.context -> Proof.method
 end
 
 structure NominalPermeq : NOMINAL_PERMEQ =
@@ -333,4 +333,4 @@
 val finite_guess_tac = finite_guess_tac NO_DEBUG_tac;
 val fresh_guess_tac = fresh_guess_tac NO_DEBUG_tac;
 
-end
\ No newline at end of file
+end
diff -r 8ff4a0ea49b2 -r ba7a7c56bed5 src/HOL/Tools/function_package/context_tree.ML
--- a/src/HOL/Tools/function_package/context_tree.ML	Wed Aug 02 22:26:40 2006 +0200
+++ b/src/HOL/Tools/function_package/context_tree.ML	Wed Aug 02 22:26:41 2006 +0200
@@ -15,7 +15,8 @@
     val cong_deps : thm -> int IntGraph.T
     val add_congs : thm list
 
-    val mk_tree: theory -> (thm * FundefCommon.depgraph) list -> term -> ProofContext.context -> term -> FundefCommon.ctx_tree
+    val mk_tree: theory -> (thm * FundefCommon.depgraph) list ->
+      term -> Proof.context -> term -> FundefCommon.ctx_tree
 
     val add_context_varnames : FundefCommon.ctx_tree -> string list -> string list
 
diff -r 8ff4a0ea49b2 -r ba7a7c56bed5 src/HOL/Tools/function_package/fundef_common.ML
--- a/src/HOL/Tools/function_package/fundef_common.ML	Wed Aug 02 22:26:40 2006 +0200
+++ b/src/HOL/Tools/function_package/fundef_common.ML	Wed Aug 02 22:26:41 2006 +0200
@@ -34,7 +34,7 @@
        glrs: (term list * term list * term * term) list,
        glrs': (term list * term list * term * term) list,
        f_def: thm,
-       ctx: ProofContext.context
+       ctx: Proof.context
      }
 
 
diff -r 8ff4a0ea49b2 -r ba7a7c56bed5 src/HOL/Tools/function_package/pattern_split.ML
--- a/src/HOL/Tools/function_package/pattern_split.ML	Wed Aug 02 22:26:40 2006 +0200
+++ b/src/HOL/Tools/function_package/pattern_split.ML	Wed Aug 02 22:26:41 2006 +0200
@@ -11,8 +11,8 @@
 
 signature FUNDEF_SPLIT = 
 sig
-  val split_some_equations : ProofContext.context -> (('a * ('b * bool)) * Term.term) list 
-                             -> (('a * 'b) * Term.term list) list
+  val split_some_equations :
+    Proof.context -> (('a * ('b * bool)) * term) list -> (('a * 'b) * term list) list
 
 end
 
@@ -115,19 +115,4 @@
       split_aux [] eqns
     end
 
-
-
-
-
-
 end
-
-
-
-
-
-
-
-
-
-
diff -r 8ff4a0ea49b2 -r ba7a7c56bed5 src/HOL/Tools/res_atp.ML
--- a/src/HOL/Tools/res_atp.ML	Wed Aug 02 22:26:40 2006 +0200
+++ b/src/HOL/Tools/res_atp.ML	Wed Aug 02 22:26:41 2006 +0200
@@ -26,8 +26,8 @@
   val vampireLimit: unit -> int
   val eproverLimit: unit -> int
   val spassLimit: unit -> int
-  val atp_method: (ProofContext.context -> thm list -> int -> Tactical.tactic) ->
-		  Method.src -> ProofContext.context -> Method.method
+  val atp_method: (Proof.context -> thm list -> int -> tactic) ->
+    Method.src -> Proof.context -> Proof.method
   val cond_rm_tmp: string -> unit
   val keep_atp_input: bool ref
   val fol_keep_types: bool ref
diff -r 8ff4a0ea49b2 -r ba7a7c56bed5 src/Provers/eqsubst.ML
--- a/src/Provers/eqsubst.ML	Wed Aug 02 22:26:40 2006 +0200
+++ b/src/Provers/eqsubst.ML	Wed Aug 02 22:26:41 2006 +0200
@@ -109,9 +109,9 @@
     val options_syntax : Args.T list -> bool * Args.T list
 
     (* Isar level hooks *)
-    val eqsubst_asm_meth : Proof.context -> int list -> Thm.thm list -> Method.method
-    val eqsubst_meth : Proof.context -> int list -> Thm.thm list -> Method.method
-    val subst_meth : Method.src -> ProofContext.context -> Method.method
+    val eqsubst_asm_meth : Proof.context -> int list -> Thm.thm list -> Proof.method
+    val eqsubst_meth : Proof.context -> int list -> Thm.thm list -> Proof.method
+    val subst_meth : Method.src -> Proof.context -> Proof.method
     val setup : theory -> theory
 
 end;
diff -r 8ff4a0ea49b2 -r ba7a7c56bed5 src/Pure/Isar/args.ML
--- a/src/Pure/Isar/args.ML	Wed Aug 02 22:26:40 2006 +0200
+++ b/src/Pure/Isar/args.ML	Wed Aug 02 22:26:41 2006 +0200
@@ -84,9 +84,9 @@
   val opt_attribs: (string -> string) -> T list -> src list * T list
   val syntax: string -> ('b * T list -> 'a * ('b * T list)) -> src -> 'b -> 'b * 'a
   val context_syntax: string -> (Context.generic * T list -> 'a * (Context.generic * T list)) ->
-    src -> ProofContext.context -> ProofContext.context * 'a
-  val pretty_src: ProofContext.context -> src -> Pretty.T
-  val pretty_attribs: ProofContext.context -> src list -> Pretty.T list
+    src -> Proof.context -> Proof.context * 'a
+  val pretty_src: Proof.context -> src -> Pretty.T
+  val pretty_attribs: Proof.context -> src list -> Pretty.T list
 end;
 
 structure Args: ARGS =
diff -r 8ff4a0ea49b2 -r ba7a7c56bed5 src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Wed Aug 02 22:26:40 2006 +0200
+++ b/src/Pure/Isar/attrib.ML	Wed Aug 02 22:26:41 2006 +0200
@@ -25,7 +25,7 @@
   val map_facts: ('a -> 'att) ->
     (('c * 'a list) * ('d * 'a list) list) list ->
     (('c * 'att list) * ('d * 'att list) list) list
-  val crude_closure: Context.proof -> src -> src
+  val crude_closure: Proof.context -> src -> src
   val add_attributes: (bstring * (src -> attribute) * string) list -> theory -> theory
   val thm: Context.generic * Args.T list -> thm * (Context.generic * Args.T list)
   val thms: Context.generic * Args.T list -> thm list * (Context.generic * Args.T list)
@@ -350,11 +350,11 @@
   let
     fun zip_vars _ [] = []
       | zip_vars (_ :: xs) ((_, NONE) :: rest) = zip_vars xs rest
-      | zip_vars ((x, _) :: xs) ((a, SOME t) :: rest) = (a, (x, t)) :: zip_vars xs rest
+      | zip_vars ((x, _) :: xs) ((arg, SOME t) :: rest) = (arg, (x, t)) :: zip_vars xs rest
       | zip_vars [] _ = error "More instantiations than variables in theorem";
     val insts =
-      zip_vars (Drule.vars_of_terms [Thm.prop_of thm]) args @
-      zip_vars (Drule.vars_of_terms [Thm.concl_of thm]) concl_args;
+      zip_vars (rev (Term.add_vars (Thm.full_prop_of thm) [])) args @
+      zip_vars (rev (Term.add_vars (Thm.concl_of thm) [])) concl_args;
   in read_instantiate insts (context, thm) end;
 
 val value =
diff -r 8ff4a0ea49b2 -r ba7a7c56bed5 src/Pure/Isar/context_rules.ML
--- a/src/Pure/Isar/context_rules.ML	Wed Aug 02 22:26:40 2006 +0200
+++ b/src/Pure/Isar/context_rules.ML	Wed Aug 02 22:26:41 2006 +0200
@@ -10,16 +10,16 @@
 sig
   type netpair
   type T
-  val netpair_bang: ProofContext.context -> netpair
-  val netpair: ProofContext.context -> netpair
+  val netpair_bang: Proof.context -> netpair
+  val netpair: Proof.context -> netpair
   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 -> ProofContext.context -> thm list list
+  val find_rules: bool -> thm list -> term -> Proof.context -> thm list list
   val print_rules: Context.generic -> unit
   val addSWrapper: ((int -> tactic) -> int -> tactic) -> theory -> theory
   val addWrapper: ((int -> tactic) -> int -> tactic) -> theory -> theory
-  val Swrap: ProofContext.context -> (int -> tactic) -> int -> tactic
-  val wrap: ProofContext.context -> (int -> tactic) -> int -> tactic
+  val Swrap: Proof.context -> (int -> tactic) -> int -> tactic
+  val wrap: Proof.context -> (int -> tactic) -> int -> tactic
   val intro_bang: int option -> attribute
   val elim_bang: int option -> attribute
   val dest_bang: int option -> attribute
diff -r 8ff4a0ea49b2 -r ba7a7c56bed5 src/Pure/Isar/method.ML
--- a/src/Pure/Isar/method.ML	Wed Aug 02 22:26:40 2006 +0200
+++ b/src/Pure/Isar/method.ML	Wed Aug 02 22:26:41 2006 +0200
@@ -12,7 +12,7 @@
   type method
   val trace_rules: bool ref
   val print_methods: theory -> unit
-  val Method: bstring -> (Args.src -> ProofContext.context -> method) -> string -> unit
+  val Method: bstring -> (Args.src -> Proof.context -> method) -> string -> unit
 end;
 
 signature METHOD =
@@ -32,31 +32,31 @@
   val SIMPLE_METHOD': ((int -> tactic) -> tactic) -> (int -> tactic) -> method
   val defer: int option -> method
   val prefer: int -> method
-  val cheating: bool -> ProofContext.context -> method
+  val cheating: bool -> Proof.context -> method
   val intro: thm list -> method
   val elim: thm list -> method
-  val unfold: thm list -> ProofContext.context -> method
-  val fold: thm list -> ProofContext.context -> method
+  val unfold: thm list -> Proof.context -> method
+  val fold: thm list -> Proof.context -> method
   val atomize: bool -> method
   val this: method
-  val fact: thm list -> ProofContext.context -> method
-  val assumption: ProofContext.context -> method
-  val close: bool -> ProofContext.context -> method
-  val trace: ProofContext.context -> thm list -> unit
+  val fact: thm list -> Proof.context -> method
+  val assumption: Proof.context -> method
+  val close: bool -> Proof.context -> method
+  val trace: Proof.context -> thm list -> unit
   val rule_tac: thm list -> thm list -> int -> tactic
-  val some_rule_tac: thm list -> ProofContext.context -> thm list -> int -> tactic
+  val some_rule_tac: thm list -> Proof.context -> thm list -> int -> tactic
   val rule: thm list -> method
   val erule: int -> thm list -> method
   val drule: int -> thm list -> method
   val frule: int -> thm list -> method
-  val iprover_tac: ProofContext.context -> int option -> int -> tactic
-  val bires_inst_tac: bool -> ProofContext.context -> (indexname * string) list ->
+  val iprover_tac: Proof.context -> int option -> int -> tactic
+  val bires_inst_tac: bool -> Proof.context -> (indexname * string) list ->
     thm -> int -> tactic
-  val set_tactic: (ProofContext.context -> thm list -> tactic) -> unit
-  val tactic: string -> ProofContext.context -> method
+  val set_tactic: (Proof.context -> thm list -> tactic) -> unit
+  val tactic: string -> Proof.context -> method
   type src
   datatype text =
-    Basic of (ProofContext.context -> method) |
+    Basic of (Proof.context -> method) |
     Source of src |
     Source_i of src |
     Then of text list |
@@ -72,45 +72,45 @@
   val sorry_text: bool -> text
   val finish_text: text option * bool -> text
   exception METHOD_FAIL of (string * Position.T) * exn
-  val method: theory -> src -> ProofContext.context -> method
-  val method_i: theory -> src -> ProofContext.context -> method
-  val add_methods: (bstring * (src -> ProofContext.context -> method) * string) list
+  val method: theory -> src -> Proof.context -> method
+  val method_i: theory -> src -> Proof.context -> method
+  val add_methods: (bstring * (src -> Proof.context -> method) * string) list
     -> theory -> theory
-  val add_method: bstring * (src -> ProofContext.context -> method) * string
+  val add_method: bstring * (src -> Proof.context -> method) * string
     -> theory -> theory
   val method_setup: bstring * string * string -> theory -> theory
   val syntax: (Context.generic * Args.T list -> 'a * (Context.generic * Args.T list))
-    -> src -> ProofContext.context -> ProofContext.context * 'a
+    -> src -> Proof.context -> Proof.context * 'a
   val simple_args: (Args.T list -> 'a * Args.T list)
-    -> ('a -> ProofContext.context -> method) -> src -> ProofContext.context -> method
-  val ctxt_args: (ProofContext.context -> method) -> src -> ProofContext.context -> method
-  val no_args: method -> src -> ProofContext.context -> method
+    -> ('a -> Proof.context -> method) -> src -> Proof.context -> method
+  val ctxt_args: (Proof.context -> method) -> src -> Proof.context -> method
+  val no_args: method -> src -> Proof.context -> method
   type modifier
   val sectioned_args: (Context.generic * Args.T list -> 'a * (Context.generic * Args.T list)) ->
     (Args.T list -> modifier * Args.T list) list ->
-    ('a -> ProofContext.context -> 'b) -> src -> ProofContext.context -> 'b
+    ('a -> Proof.context -> 'b) -> src -> Proof.context -> 'b
   val bang_sectioned_args:
     (Args.T list -> modifier * Args.T list) list ->
-    (thm list -> ProofContext.context -> 'a) -> src -> ProofContext.context -> 'a
+    (thm list -> Proof.context -> 'a) -> src -> Proof.context -> 'a
   val bang_sectioned_args':
     (Args.T list -> modifier * Args.T list) list ->
     (Context.generic * Args.T list -> 'a * (Context.generic * Args.T list)) ->
-    ('a -> thm list -> ProofContext.context -> 'b) -> src -> ProofContext.context -> 'b
+    ('a -> thm list -> Proof.context -> 'b) -> src -> Proof.context -> 'b
   val only_sectioned_args:
     (Args.T list -> modifier * Args.T list) list ->
-    (ProofContext.context -> 'a) -> src -> ProofContext.context -> 'a
-  val thms_ctxt_args: (thm list -> ProofContext.context -> 'a) -> src ->
-    ProofContext.context -> 'a
-  val thms_args: (thm list -> 'a) -> src -> ProofContext.context -> 'a
-  val thm_args: (thm -> 'a) -> src -> ProofContext.context -> 'a
+    (Proof.context -> 'a) -> src -> Proof.context -> 'a
+  val thms_ctxt_args: (thm list -> Proof.context -> 'a) -> src ->
+    Proof.context -> 'a
+  val thms_args: (thm list -> 'a) -> src -> Proof.context -> 'a
+  val thm_args: (thm -> 'a) -> src -> Proof.context -> 'a
   val goal_args: (Args.T list -> 'a * Args.T list) -> ('a -> int -> tactic)
-    -> src -> ProofContext.context -> method
+    -> src -> Proof.context -> method
   val goal_args': (Context.generic * Args.T list -> 'a * (Context.generic * Args.T list))
-    -> ('a -> int -> tactic) -> src -> ProofContext.context -> method
+    -> ('a -> int -> tactic) -> src -> Proof.context -> method
   val goal_args_ctxt: (Args.T list -> 'a * Args.T list) ->
-    (ProofContext.context -> 'a -> int -> tactic) -> src -> ProofContext.context -> method
+    (Proof.context -> 'a -> int -> tactic) -> src -> Proof.context -> method
   val goal_args_ctxt': (Context.generic * Args.T list -> 'a * (Context.generic * Args.T list)) ->
-    (ProofContext.context -> 'a -> int -> tactic) -> src -> ProofContext.context -> method
+    (Proof.context -> 'a -> int -> tactic) -> src -> Proof.context -> method
 end;
 
 structure Method: METHOD =
@@ -467,12 +467,12 @@
 
 (* ML tactics *)
 
-val tactic_ref = ref ((fn _ => raise Match): ProofContext.context -> thm list -> tactic);
+val tactic_ref = ref ((fn _ => raise Match): Proof.context -> thm list -> tactic);
 fun set_tactic f = tactic_ref := f;
 
 fun tactic txt ctxt = METHOD (fn facts =>
   (Context.use_mltext
-    ("let fun tactic (ctxt: ProofContext.context) (facts: thm list) : tactic = \
+    ("let fun tactic (ctxt: Proof.context) (facts: thm list) : tactic = \
        \let val thm = ProofContext.get_thm_closure ctxt o PureThy.Name\n\
        \  and thms = ProofContext.get_thms_closure ctxt o PureThy.Name in\n"
        ^ txt ^
@@ -489,7 +489,7 @@
 type src = Args.src;
 
 datatype text =
-  Basic of (ProofContext.context -> method) |
+  Basic of (Proof.context -> method) |
   Source of src |
   Source_i of src |
   Then of text list |
@@ -514,7 +514,7 @@
 structure MethodsData = TheoryDataFun
 (struct
   val name = "Isar/methods";
-  type T = (((src -> ProofContext.context -> method) * string) * stamp) NameSpace.table;
+  type T = (((src -> Proof.context -> method) * string) * stamp) NameSpace.table;
 
   val empty = NameSpace.empty_table;
   val copy = I;
@@ -577,7 +577,7 @@
   Context.use_let
     "val thm = PureThy.get_thm_closure (Context.the_context ()) o PureThy.Name;\n\
     \val thms = PureThy.get_thms_closure (Context.the_context ()) o PureThy.Name;\n\
-    \val method: bstring * (Method.src -> ProofContext.context -> Proof.method) * string"
+    \val method: bstring * (Method.src -> Proof.context -> Proof.method) * string"
     "Method.add_method method"
     ("(" ^ Library.quote name ^ ", " ^ txt ^ ", " ^ Library.quote cmt ^ ")");
 
@@ -592,7 +592,7 @@
 fun simple_args scan f src ctxt : method =
   #2 (syntax (Scan.lift (scan >> (fn x => f x ctxt))) src ctxt);
 
-fun ctxt_args (f: ProofContext.context -> method) src ctxt =
+fun ctxt_args (f: Proof.context -> method) src ctxt =
   #2 (syntax (Scan.succeed (f ctxt)) src ctxt);
 
 fun no_args m = ctxt_args (K m);
@@ -600,7 +600,7 @@
 
 (* sections *)
 
-type modifier = (ProofContext.context -> ProofContext.context) * attribute;
+type modifier = (Proof.context -> Proof.context) * attribute;
 
 local
 
@@ -643,7 +643,7 @@
 
 fun modifier name kind kind' att =
   Args.$$$ name |-- (kind >> K NONE || kind' |-- Args.nat --| Args.colon >> SOME)
-    >> (pair (I: ProofContext.context -> ProofContext.context) o att);
+    >> (pair (I: Proof.context -> Proof.context) o att);
 
 val iprover_modifiers =
  [modifier destN Args.bang_colon Args.bang ContextRules.dest_bang,
diff -r 8ff4a0ea49b2 -r ba7a7c56bed5 src/Pure/Isar/rule_cases.ML
--- a/src/Pure/Isar/rule_cases.ML	Wed Aug 02 22:26:40 2006 +0200
+++ b/src/Pure/Isar/rule_cases.ML	Wed Aug 02 22:26:41 2006 +0200
@@ -42,8 +42,8 @@
   val get: thm -> (string * string list) list * int
   val rename_params: string list list -> thm -> thm
   val params: string list list -> attribute
-  val mutual_rule: Context.proof -> thm list -> (int list * thm) option
-  val strict_mutual_rule: Context.proof -> thm list -> int list * thm
+  val mutual_rule: Proof.context -> thm list -> (int list * thm) option
+  val strict_mutual_rule: Proof.context -> thm list -> int list * thm
 end;
 
 structure RuleCases: RULE_CASES =
diff -r 8ff4a0ea49b2 -r ba7a7c56bed5 src/Pure/Isar/skip_proof.ML
--- a/src/Pure/Isar/skip_proof.ML	Wed Aug 02 22:26:40 2006 +0200
+++ b/src/Pure/Isar/skip_proof.ML	Wed Aug 02 22:26:41 2006 +0200
@@ -9,8 +9,8 @@
 sig
   val make_thm: theory -> term -> thm
   val cheat_tac: theory -> tactic
-  val prove: ProofContext.context -> string list -> term list -> term ->
-    ({prems: thm list, context: Context.proof} -> tactic) -> thm
+  val prove: Proof.context -> string list -> term list -> term ->
+    ({prems: thm list, context: Proof.context} -> tactic) -> thm
 end;
 
 structure SkipProof: SKIP_PROOF =
diff -r 8ff4a0ea49b2 -r ba7a7c56bed5 src/Pure/Tools/class_package.ML
--- a/src/Pure/Tools/class_package.ML	Wed Aug 02 22:26:40 2006 +0200
+++ b/src/Pure/Tools/class_package.ML	Wed Aug 02 22:26:41 2006 +0200
@@ -8,9 +8,9 @@
 signature CLASS_PACKAGE =
 sig
   val class: bstring -> class list -> Element.context list -> theory
-    -> ProofContext.context * theory
+    -> Proof.context * theory
   val class_i: bstring -> class list -> Element.context_i list -> theory
-    -> ProofContext.context * theory
+    -> Proof.context * theory
   (*FIXME: in _i variants, bstring should be bstring option*)
   val instance_arity: ((xstring * string list) * string) list
     -> bstring * Attrib.src list -> ((bstring * Attrib.src list) * string) list
diff -r 8ff4a0ea49b2 -r ba7a7c56bed5 src/Pure/meta_simplifier.ML
--- a/src/Pure/meta_simplifier.ML	Wed Aug 02 22:26:40 2006 +0200
+++ b/src/Pure/meta_simplifier.ML	Wed Aug 02 22:26:41 2006 +0200
@@ -28,7 +28,7 @@
    {rules: rrule Net.net,
     prems: thm list,
     bounds: int * ((string * typ) * string) list,
-    context: Context.proof option} *
+    context: Proof.context option} *
    {congs: (string * cong) list * string list,
     procs: proc Net.net,
     mk_rews:
@@ -88,8 +88,8 @@
   val simproc: theory -> string -> string list
     -> (theory -> simpset -> term -> thm option) -> simproc
   val inherit_context: simpset -> simpset -> simpset
-  val the_context: simpset -> Context.proof
-  val context: Context.proof -> simpset -> simpset
+  val the_context: simpset -> Proof.context
+  val context: Proof.context -> simpset -> simpset
   val theory_context: theory  -> simpset -> simpset
   val debug_bounds: bool ref
   val set_reorient: (theory -> term list -> term -> term -> bool) -> simpset -> simpset
@@ -175,7 +175,7 @@
    {rules: rrule Net.net,
     prems: thm list,
     bounds: int * ((string * typ) * string) list,
-    context: Context.proof option} *
+    context: Proof.context option} *
    {congs: (string * cong) list * string list,
     procs: proc Net.net,
     mk_rews: mk_rews,
diff -r 8ff4a0ea49b2 -r ba7a7c56bed5 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Wed Aug 02 22:26:40 2006 +0200
+++ b/src/Pure/thm.ML	Wed Aug 02 22:26:41 2006 +0200
@@ -142,7 +142,7 @@
   val rule_attribute: (Context.generic -> thm -> thm) -> attribute
   val declaration_attribute: (thm -> Context.generic -> Context.generic) -> attribute
   val theory_attributes: attribute list -> theory * thm -> theory * thm
-  val proof_attributes: attribute list -> Context.proof * thm -> Context.proof * thm
+  val proof_attributes: attribute list -> Proof.context * thm -> Proof.context * thm
   val no_attributes: 'a -> 'a * 'b list
   val simple_fact: 'a -> ('a * 'b list) list
   val terms_of_tpairs: (term * term) list -> term list