normalized Proof.context/method type aliases;
authorwenzelm
Wed Aug 02 22:26:41 2006 +0200 (2006-08-02)
changeset 20289ba7a7c56bed5
parent 20288 8ff4a0ea49b2
child 20290 3f886c176c9b
normalized Proof.context/method type aliases;
src/HOL/Nominal/nominal_permeq.ML
src/HOL/Tools/function_package/context_tree.ML
src/HOL/Tools/function_package/fundef_common.ML
src/HOL/Tools/function_package/pattern_split.ML
src/HOL/Tools/res_atp.ML
src/Provers/eqsubst.ML
src/Pure/Isar/args.ML
src/Pure/Isar/attrib.ML
src/Pure/Isar/context_rules.ML
src/Pure/Isar/method.ML
src/Pure/Isar/rule_cases.ML
src/Pure/Isar/skip_proof.ML
src/Pure/Tools/class_package.ML
src/Pure/meta_simplifier.ML
src/Pure/thm.ML
     1.1 --- a/src/HOL/Nominal/nominal_permeq.ML	Wed Aug 02 22:26:40 2006 +0200
     1.2 +++ b/src/HOL/Nominal/nominal_permeq.ML	Wed Aug 02 22:26:41 2006 +0200
     1.3 @@ -14,16 +14,16 @@
     1.4    val finite_guess_tac : simpset -> int -> tactic
     1.5    val fresh_guess_tac : simpset -> int -> tactic
     1.6  
     1.7 -  val perm_eq_meth : Method.src -> ProofContext.context -> Method.method
     1.8 -  val perm_eq_meth_debug : Method.src -> ProofContext.context -> Method.method
     1.9 -  val perm_full_eq_meth : Method.src -> ProofContext.context -> Method.method
    1.10 -  val perm_full_eq_meth_debug : Method.src -> ProofContext.context -> Method.method
    1.11 -  val supports_meth : Method.src -> ProofContext.context -> Method.method
    1.12 -  val supports_meth_debug : Method.src -> ProofContext.context -> Method.method
    1.13 -  val finite_gs_meth : Method.src -> ProofContext.context -> Method.method
    1.14 -  val finite_gs_meth_debug : Method.src -> ProofContext.context -> Method.method
    1.15 -  val fresh_gs_meth : Method.src -> ProofContext.context -> Method.method
    1.16 -  val fresh_gs_meth_debug : Method.src -> ProofContext.context -> Method.method
    1.17 +  val perm_eq_meth : Method.src -> Proof.context -> Proof.method
    1.18 +  val perm_eq_meth_debug : Method.src -> Proof.context -> Proof.method
    1.19 +  val perm_full_eq_meth : Method.src -> Proof.context -> Proof.method
    1.20 +  val perm_full_eq_meth_debug : Method.src -> Proof.context -> Proof.method
    1.21 +  val supports_meth : Method.src -> Proof.context -> Proof.method
    1.22 +  val supports_meth_debug : Method.src -> Proof.context -> Proof.method
    1.23 +  val finite_gs_meth : Method.src -> Proof.context -> Proof.method
    1.24 +  val finite_gs_meth_debug : Method.src -> Proof.context -> Proof.method
    1.25 +  val fresh_gs_meth : Method.src -> Proof.context -> Proof.method
    1.26 +  val fresh_gs_meth_debug : Method.src -> Proof.context -> Proof.method
    1.27  end
    1.28  
    1.29  structure NominalPermeq : NOMINAL_PERMEQ =
    1.30 @@ -333,4 +333,4 @@
    1.31  val finite_guess_tac = finite_guess_tac NO_DEBUG_tac;
    1.32  val fresh_guess_tac = fresh_guess_tac NO_DEBUG_tac;
    1.33  
    1.34 -end
    1.35 \ No newline at end of file
    1.36 +end
     2.1 --- a/src/HOL/Tools/function_package/context_tree.ML	Wed Aug 02 22:26:40 2006 +0200
     2.2 +++ b/src/HOL/Tools/function_package/context_tree.ML	Wed Aug 02 22:26:41 2006 +0200
     2.3 @@ -15,7 +15,8 @@
     2.4      val cong_deps : thm -> int IntGraph.T
     2.5      val add_congs : thm list
     2.6  
     2.7 -    val mk_tree: theory -> (thm * FundefCommon.depgraph) list -> term -> ProofContext.context -> term -> FundefCommon.ctx_tree
     2.8 +    val mk_tree: theory -> (thm * FundefCommon.depgraph) list ->
     2.9 +      term -> Proof.context -> term -> FundefCommon.ctx_tree
    2.10  
    2.11      val add_context_varnames : FundefCommon.ctx_tree -> string list -> string list
    2.12  
     3.1 --- a/src/HOL/Tools/function_package/fundef_common.ML	Wed Aug 02 22:26:40 2006 +0200
     3.2 +++ b/src/HOL/Tools/function_package/fundef_common.ML	Wed Aug 02 22:26:41 2006 +0200
     3.3 @@ -34,7 +34,7 @@
     3.4         glrs: (term list * term list * term * term) list,
     3.5         glrs': (term list * term list * term * term) list,
     3.6         f_def: thm,
     3.7 -       ctx: ProofContext.context
     3.8 +       ctx: Proof.context
     3.9       }
    3.10  
    3.11  
     4.1 --- a/src/HOL/Tools/function_package/pattern_split.ML	Wed Aug 02 22:26:40 2006 +0200
     4.2 +++ b/src/HOL/Tools/function_package/pattern_split.ML	Wed Aug 02 22:26:41 2006 +0200
     4.3 @@ -11,8 +11,8 @@
     4.4  
     4.5  signature FUNDEF_SPLIT = 
     4.6  sig
     4.7 -  val split_some_equations : ProofContext.context -> (('a * ('b * bool)) * Term.term) list 
     4.8 -                             -> (('a * 'b) * Term.term list) list
     4.9 +  val split_some_equations :
    4.10 +    Proof.context -> (('a * ('b * bool)) * term) list -> (('a * 'b) * term list) list
    4.11  
    4.12  end
    4.13  
    4.14 @@ -115,19 +115,4 @@
    4.15        split_aux [] eqns
    4.16      end
    4.17  
    4.18 -
    4.19 -
    4.20 -
    4.21 -
    4.22 -
    4.23  end
    4.24 -
    4.25 -
    4.26 -
    4.27 -
    4.28 -
    4.29 -
    4.30 -
    4.31 -
    4.32 -
    4.33 -
     5.1 --- a/src/HOL/Tools/res_atp.ML	Wed Aug 02 22:26:40 2006 +0200
     5.2 +++ b/src/HOL/Tools/res_atp.ML	Wed Aug 02 22:26:41 2006 +0200
     5.3 @@ -26,8 +26,8 @@
     5.4    val vampireLimit: unit -> int
     5.5    val eproverLimit: unit -> int
     5.6    val spassLimit: unit -> int
     5.7 -  val atp_method: (ProofContext.context -> thm list -> int -> Tactical.tactic) ->
     5.8 -		  Method.src -> ProofContext.context -> Method.method
     5.9 +  val atp_method: (Proof.context -> thm list -> int -> tactic) ->
    5.10 +    Method.src -> Proof.context -> Proof.method
    5.11    val cond_rm_tmp: string -> unit
    5.12    val keep_atp_input: bool ref
    5.13    val fol_keep_types: bool ref
     6.1 --- a/src/Provers/eqsubst.ML	Wed Aug 02 22:26:40 2006 +0200
     6.2 +++ b/src/Provers/eqsubst.ML	Wed Aug 02 22:26:41 2006 +0200
     6.3 @@ -109,9 +109,9 @@
     6.4      val options_syntax : Args.T list -> bool * Args.T list
     6.5  
     6.6      (* Isar level hooks *)
     6.7 -    val eqsubst_asm_meth : Proof.context -> int list -> Thm.thm list -> Method.method
     6.8 -    val eqsubst_meth : Proof.context -> int list -> Thm.thm list -> Method.method
     6.9 -    val subst_meth : Method.src -> ProofContext.context -> Method.method
    6.10 +    val eqsubst_asm_meth : Proof.context -> int list -> Thm.thm list -> Proof.method
    6.11 +    val eqsubst_meth : Proof.context -> int list -> Thm.thm list -> Proof.method
    6.12 +    val subst_meth : Method.src -> Proof.context -> Proof.method
    6.13      val setup : theory -> theory
    6.14  
    6.15  end;
     7.1 --- a/src/Pure/Isar/args.ML	Wed Aug 02 22:26:40 2006 +0200
     7.2 +++ b/src/Pure/Isar/args.ML	Wed Aug 02 22:26:41 2006 +0200
     7.3 @@ -84,9 +84,9 @@
     7.4    val opt_attribs: (string -> string) -> T list -> src list * T list
     7.5    val syntax: string -> ('b * T list -> 'a * ('b * T list)) -> src -> 'b -> 'b * 'a
     7.6    val context_syntax: string -> (Context.generic * T list -> 'a * (Context.generic * T list)) ->
     7.7 -    src -> ProofContext.context -> ProofContext.context * 'a
     7.8 -  val pretty_src: ProofContext.context -> src -> Pretty.T
     7.9 -  val pretty_attribs: ProofContext.context -> src list -> Pretty.T list
    7.10 +    src -> Proof.context -> Proof.context * 'a
    7.11 +  val pretty_src: Proof.context -> src -> Pretty.T
    7.12 +  val pretty_attribs: Proof.context -> src list -> Pretty.T list
    7.13  end;
    7.14  
    7.15  structure Args: ARGS =
     8.1 --- a/src/Pure/Isar/attrib.ML	Wed Aug 02 22:26:40 2006 +0200
     8.2 +++ b/src/Pure/Isar/attrib.ML	Wed Aug 02 22:26:41 2006 +0200
     8.3 @@ -25,7 +25,7 @@
     8.4    val map_facts: ('a -> 'att) ->
     8.5      (('c * 'a list) * ('d * 'a list) list) list ->
     8.6      (('c * 'att list) * ('d * 'att list) list) list
     8.7 -  val crude_closure: Context.proof -> src -> src
     8.8 +  val crude_closure: Proof.context -> src -> src
     8.9    val add_attributes: (bstring * (src -> attribute) * string) list -> theory -> theory
    8.10    val thm: Context.generic * Args.T list -> thm * (Context.generic * Args.T list)
    8.11    val thms: Context.generic * Args.T list -> thm list * (Context.generic * Args.T list)
    8.12 @@ -350,11 +350,11 @@
    8.13    let
    8.14      fun zip_vars _ [] = []
    8.15        | zip_vars (_ :: xs) ((_, NONE) :: rest) = zip_vars xs rest
    8.16 -      | zip_vars ((x, _) :: xs) ((a, SOME t) :: rest) = (a, (x, t)) :: zip_vars xs rest
    8.17 +      | zip_vars ((x, _) :: xs) ((arg, SOME t) :: rest) = (arg, (x, t)) :: zip_vars xs rest
    8.18        | zip_vars [] _ = error "More instantiations than variables in theorem";
    8.19      val insts =
    8.20 -      zip_vars (Drule.vars_of_terms [Thm.prop_of thm]) args @
    8.21 -      zip_vars (Drule.vars_of_terms [Thm.concl_of thm]) concl_args;
    8.22 +      zip_vars (rev (Term.add_vars (Thm.full_prop_of thm) [])) args @
    8.23 +      zip_vars (rev (Term.add_vars (Thm.concl_of thm) [])) concl_args;
    8.24    in read_instantiate insts (context, thm) end;
    8.25  
    8.26  val value =
     9.1 --- a/src/Pure/Isar/context_rules.ML	Wed Aug 02 22:26:40 2006 +0200
     9.2 +++ b/src/Pure/Isar/context_rules.ML	Wed Aug 02 22:26:41 2006 +0200
     9.3 @@ -10,16 +10,16 @@
     9.4  sig
     9.5    type netpair
     9.6    type T
     9.7 -  val netpair_bang: ProofContext.context -> netpair
     9.8 -  val netpair: ProofContext.context -> netpair
     9.9 +  val netpair_bang: Proof.context -> netpair
    9.10 +  val netpair: Proof.context -> netpair
    9.11    val orderlist: ((int * int) * 'a) list -> 'a list
    9.12    val find_rules_netpair: bool -> thm list -> term -> netpair -> thm list
    9.13 -  val find_rules: bool -> thm list -> term -> ProofContext.context -> thm list list
    9.14 +  val find_rules: bool -> thm list -> term -> Proof.context -> thm list list
    9.15    val print_rules: Context.generic -> unit
    9.16    val addSWrapper: ((int -> tactic) -> int -> tactic) -> theory -> theory
    9.17    val addWrapper: ((int -> tactic) -> int -> tactic) -> theory -> theory
    9.18 -  val Swrap: ProofContext.context -> (int -> tactic) -> int -> tactic
    9.19 -  val wrap: ProofContext.context -> (int -> tactic) -> int -> tactic
    9.20 +  val Swrap: Proof.context -> (int -> tactic) -> int -> tactic
    9.21 +  val wrap: Proof.context -> (int -> tactic) -> int -> tactic
    9.22    val intro_bang: int option -> attribute
    9.23    val elim_bang: int option -> attribute
    9.24    val dest_bang: int option -> attribute
    10.1 --- a/src/Pure/Isar/method.ML	Wed Aug 02 22:26:40 2006 +0200
    10.2 +++ b/src/Pure/Isar/method.ML	Wed Aug 02 22:26:41 2006 +0200
    10.3 @@ -12,7 +12,7 @@
    10.4    type method
    10.5    val trace_rules: bool ref
    10.6    val print_methods: theory -> unit
    10.7 -  val Method: bstring -> (Args.src -> ProofContext.context -> method) -> string -> unit
    10.8 +  val Method: bstring -> (Args.src -> Proof.context -> method) -> string -> unit
    10.9  end;
   10.10  
   10.11  signature METHOD =
   10.12 @@ -32,31 +32,31 @@
   10.13    val SIMPLE_METHOD': ((int -> tactic) -> tactic) -> (int -> tactic) -> method
   10.14    val defer: int option -> method
   10.15    val prefer: int -> method
   10.16 -  val cheating: bool -> ProofContext.context -> method
   10.17 +  val cheating: bool -> Proof.context -> method
   10.18    val intro: thm list -> method
   10.19    val elim: thm list -> method
   10.20 -  val unfold: thm list -> ProofContext.context -> method
   10.21 -  val fold: thm list -> ProofContext.context -> method
   10.22 +  val unfold: thm list -> Proof.context -> method
   10.23 +  val fold: thm list -> Proof.context -> method
   10.24    val atomize: bool -> method
   10.25    val this: method
   10.26 -  val fact: thm list -> ProofContext.context -> method
   10.27 -  val assumption: ProofContext.context -> method
   10.28 -  val close: bool -> ProofContext.context -> method
   10.29 -  val trace: ProofContext.context -> thm list -> unit
   10.30 +  val fact: thm list -> Proof.context -> method
   10.31 +  val assumption: Proof.context -> method
   10.32 +  val close: bool -> Proof.context -> method
   10.33 +  val trace: Proof.context -> thm list -> unit
   10.34    val rule_tac: thm list -> thm list -> int -> tactic
   10.35 -  val some_rule_tac: thm list -> ProofContext.context -> thm list -> int -> tactic
   10.36 +  val some_rule_tac: thm list -> Proof.context -> thm list -> int -> tactic
   10.37    val rule: thm list -> method
   10.38    val erule: int -> thm list -> method
   10.39    val drule: int -> thm list -> method
   10.40    val frule: int -> thm list -> method
   10.41 -  val iprover_tac: ProofContext.context -> int option -> int -> tactic
   10.42 -  val bires_inst_tac: bool -> ProofContext.context -> (indexname * string) list ->
   10.43 +  val iprover_tac: Proof.context -> int option -> int -> tactic
   10.44 +  val bires_inst_tac: bool -> Proof.context -> (indexname * string) list ->
   10.45      thm -> int -> tactic
   10.46 -  val set_tactic: (ProofContext.context -> thm list -> tactic) -> unit
   10.47 -  val tactic: string -> ProofContext.context -> method
   10.48 +  val set_tactic: (Proof.context -> thm list -> tactic) -> unit
   10.49 +  val tactic: string -> Proof.context -> method
   10.50    type src
   10.51    datatype text =
   10.52 -    Basic of (ProofContext.context -> method) |
   10.53 +    Basic of (Proof.context -> method) |
   10.54      Source of src |
   10.55      Source_i of src |
   10.56      Then of text list |
   10.57 @@ -72,45 +72,45 @@
   10.58    val sorry_text: bool -> text
   10.59    val finish_text: text option * bool -> text
   10.60    exception METHOD_FAIL of (string * Position.T) * exn
   10.61 -  val method: theory -> src -> ProofContext.context -> method
   10.62 -  val method_i: theory -> src -> ProofContext.context -> method
   10.63 -  val add_methods: (bstring * (src -> ProofContext.context -> method) * string) list
   10.64 +  val method: theory -> src -> Proof.context -> method
   10.65 +  val method_i: theory -> src -> Proof.context -> method
   10.66 +  val add_methods: (bstring * (src -> Proof.context -> method) * string) list
   10.67      -> theory -> theory
   10.68 -  val add_method: bstring * (src -> ProofContext.context -> method) * string
   10.69 +  val add_method: bstring * (src -> Proof.context -> method) * string
   10.70      -> theory -> theory
   10.71    val method_setup: bstring * string * string -> theory -> theory
   10.72    val syntax: (Context.generic * Args.T list -> 'a * (Context.generic * Args.T list))
   10.73 -    -> src -> ProofContext.context -> ProofContext.context * 'a
   10.74 +    -> src -> Proof.context -> Proof.context * 'a
   10.75    val simple_args: (Args.T list -> 'a * Args.T list)
   10.76 -    -> ('a -> ProofContext.context -> method) -> src -> ProofContext.context -> method
   10.77 -  val ctxt_args: (ProofContext.context -> method) -> src -> ProofContext.context -> method
   10.78 -  val no_args: method -> src -> ProofContext.context -> method
   10.79 +    -> ('a -> Proof.context -> method) -> src -> Proof.context -> method
   10.80 +  val ctxt_args: (Proof.context -> method) -> src -> Proof.context -> method
   10.81 +  val no_args: method -> src -> Proof.context -> method
   10.82    type modifier
   10.83    val sectioned_args: (Context.generic * Args.T list -> 'a * (Context.generic * Args.T list)) ->
   10.84      (Args.T list -> modifier * Args.T list) list ->
   10.85 -    ('a -> ProofContext.context -> 'b) -> src -> ProofContext.context -> 'b
   10.86 +    ('a -> Proof.context -> 'b) -> src -> Proof.context -> 'b
   10.87    val bang_sectioned_args:
   10.88      (Args.T list -> modifier * Args.T list) list ->
   10.89 -    (thm list -> ProofContext.context -> 'a) -> src -> ProofContext.context -> 'a
   10.90 +    (thm list -> Proof.context -> 'a) -> src -> Proof.context -> 'a
   10.91    val bang_sectioned_args':
   10.92      (Args.T list -> modifier * Args.T list) list ->
   10.93      (Context.generic * Args.T list -> 'a * (Context.generic * Args.T list)) ->
   10.94 -    ('a -> thm list -> ProofContext.context -> 'b) -> src -> ProofContext.context -> 'b
   10.95 +    ('a -> thm list -> Proof.context -> 'b) -> src -> Proof.context -> 'b
   10.96    val only_sectioned_args:
   10.97      (Args.T list -> modifier * Args.T list) list ->
   10.98 -    (ProofContext.context -> 'a) -> src -> ProofContext.context -> 'a
   10.99 -  val thms_ctxt_args: (thm list -> ProofContext.context -> 'a) -> src ->
  10.100 -    ProofContext.context -> 'a
  10.101 -  val thms_args: (thm list -> 'a) -> src -> ProofContext.context -> 'a
  10.102 -  val thm_args: (thm -> 'a) -> src -> ProofContext.context -> 'a
  10.103 +    (Proof.context -> 'a) -> src -> Proof.context -> 'a
  10.104 +  val thms_ctxt_args: (thm list -> Proof.context -> 'a) -> src ->
  10.105 +    Proof.context -> 'a
  10.106 +  val thms_args: (thm list -> 'a) -> src -> Proof.context -> 'a
  10.107 +  val thm_args: (thm -> 'a) -> src -> Proof.context -> 'a
  10.108    val goal_args: (Args.T list -> 'a * Args.T list) -> ('a -> int -> tactic)
  10.109 -    -> src -> ProofContext.context -> method
  10.110 +    -> src -> Proof.context -> method
  10.111    val goal_args': (Context.generic * Args.T list -> 'a * (Context.generic * Args.T list))
  10.112 -    -> ('a -> int -> tactic) -> src -> ProofContext.context -> method
  10.113 +    -> ('a -> int -> tactic) -> src -> Proof.context -> method
  10.114    val goal_args_ctxt: (Args.T list -> 'a * Args.T list) ->
  10.115 -    (ProofContext.context -> 'a -> int -> tactic) -> src -> ProofContext.context -> method
  10.116 +    (Proof.context -> 'a -> int -> tactic) -> src -> Proof.context -> method
  10.117    val goal_args_ctxt': (Context.generic * Args.T list -> 'a * (Context.generic * Args.T list)) ->
  10.118 -    (ProofContext.context -> 'a -> int -> tactic) -> src -> ProofContext.context -> method
  10.119 +    (Proof.context -> 'a -> int -> tactic) -> src -> Proof.context -> method
  10.120  end;
  10.121  
  10.122  structure Method: METHOD =
  10.123 @@ -467,12 +467,12 @@
  10.124  
  10.125  (* ML tactics *)
  10.126  
  10.127 -val tactic_ref = ref ((fn _ => raise Match): ProofContext.context -> thm list -> tactic);
  10.128 +val tactic_ref = ref ((fn _ => raise Match): Proof.context -> thm list -> tactic);
  10.129  fun set_tactic f = tactic_ref := f;
  10.130  
  10.131  fun tactic txt ctxt = METHOD (fn facts =>
  10.132    (Context.use_mltext
  10.133 -    ("let fun tactic (ctxt: ProofContext.context) (facts: thm list) : tactic = \
  10.134 +    ("let fun tactic (ctxt: Proof.context) (facts: thm list) : tactic = \
  10.135         \let val thm = ProofContext.get_thm_closure ctxt o PureThy.Name\n\
  10.136         \  and thms = ProofContext.get_thms_closure ctxt o PureThy.Name in\n"
  10.137         ^ txt ^
  10.138 @@ -489,7 +489,7 @@
  10.139  type src = Args.src;
  10.140  
  10.141  datatype text =
  10.142 -  Basic of (ProofContext.context -> method) |
  10.143 +  Basic of (Proof.context -> method) |
  10.144    Source of src |
  10.145    Source_i of src |
  10.146    Then of text list |
  10.147 @@ -514,7 +514,7 @@
  10.148  structure MethodsData = TheoryDataFun
  10.149  (struct
  10.150    val name = "Isar/methods";
  10.151 -  type T = (((src -> ProofContext.context -> method) * string) * stamp) NameSpace.table;
  10.152 +  type T = (((src -> Proof.context -> method) * string) * stamp) NameSpace.table;
  10.153  
  10.154    val empty = NameSpace.empty_table;
  10.155    val copy = I;
  10.156 @@ -577,7 +577,7 @@
  10.157    Context.use_let
  10.158      "val thm = PureThy.get_thm_closure (Context.the_context ()) o PureThy.Name;\n\
  10.159      \val thms = PureThy.get_thms_closure (Context.the_context ()) o PureThy.Name;\n\
  10.160 -    \val method: bstring * (Method.src -> ProofContext.context -> Proof.method) * string"
  10.161 +    \val method: bstring * (Method.src -> Proof.context -> Proof.method) * string"
  10.162      "Method.add_method method"
  10.163      ("(" ^ Library.quote name ^ ", " ^ txt ^ ", " ^ Library.quote cmt ^ ")");
  10.164  
  10.165 @@ -592,7 +592,7 @@
  10.166  fun simple_args scan f src ctxt : method =
  10.167    #2 (syntax (Scan.lift (scan >> (fn x => f x ctxt))) src ctxt);
  10.168  
  10.169 -fun ctxt_args (f: ProofContext.context -> method) src ctxt =
  10.170 +fun ctxt_args (f: Proof.context -> method) src ctxt =
  10.171    #2 (syntax (Scan.succeed (f ctxt)) src ctxt);
  10.172  
  10.173  fun no_args m = ctxt_args (K m);
  10.174 @@ -600,7 +600,7 @@
  10.175  
  10.176  (* sections *)
  10.177  
  10.178 -type modifier = (ProofContext.context -> ProofContext.context) * attribute;
  10.179 +type modifier = (Proof.context -> Proof.context) * attribute;
  10.180  
  10.181  local
  10.182  
  10.183 @@ -643,7 +643,7 @@
  10.184  
  10.185  fun modifier name kind kind' att =
  10.186    Args.$$$ name |-- (kind >> K NONE || kind' |-- Args.nat --| Args.colon >> SOME)
  10.187 -    >> (pair (I: ProofContext.context -> ProofContext.context) o att);
  10.188 +    >> (pair (I: Proof.context -> Proof.context) o att);
  10.189  
  10.190  val iprover_modifiers =
  10.191   [modifier destN Args.bang_colon Args.bang ContextRules.dest_bang,
    11.1 --- a/src/Pure/Isar/rule_cases.ML	Wed Aug 02 22:26:40 2006 +0200
    11.2 +++ b/src/Pure/Isar/rule_cases.ML	Wed Aug 02 22:26:41 2006 +0200
    11.3 @@ -42,8 +42,8 @@
    11.4    val get: thm -> (string * string list) list * int
    11.5    val rename_params: string list list -> thm -> thm
    11.6    val params: string list list -> attribute
    11.7 -  val mutual_rule: Context.proof -> thm list -> (int list * thm) option
    11.8 -  val strict_mutual_rule: Context.proof -> thm list -> int list * thm
    11.9 +  val mutual_rule: Proof.context -> thm list -> (int list * thm) option
   11.10 +  val strict_mutual_rule: Proof.context -> thm list -> int list * thm
   11.11  end;
   11.12  
   11.13  structure RuleCases: RULE_CASES =
    12.1 --- a/src/Pure/Isar/skip_proof.ML	Wed Aug 02 22:26:40 2006 +0200
    12.2 +++ b/src/Pure/Isar/skip_proof.ML	Wed Aug 02 22:26:41 2006 +0200
    12.3 @@ -9,8 +9,8 @@
    12.4  sig
    12.5    val make_thm: theory -> term -> thm
    12.6    val cheat_tac: theory -> tactic
    12.7 -  val prove: ProofContext.context -> string list -> term list -> term ->
    12.8 -    ({prems: thm list, context: Context.proof} -> tactic) -> thm
    12.9 +  val prove: Proof.context -> string list -> term list -> term ->
   12.10 +    ({prems: thm list, context: Proof.context} -> tactic) -> thm
   12.11  end;
   12.12  
   12.13  structure SkipProof: SKIP_PROOF =
    13.1 --- a/src/Pure/Tools/class_package.ML	Wed Aug 02 22:26:40 2006 +0200
    13.2 +++ b/src/Pure/Tools/class_package.ML	Wed Aug 02 22:26:41 2006 +0200
    13.3 @@ -8,9 +8,9 @@
    13.4  signature CLASS_PACKAGE =
    13.5  sig
    13.6    val class: bstring -> class list -> Element.context list -> theory
    13.7 -    -> ProofContext.context * theory
    13.8 +    -> Proof.context * theory
    13.9    val class_i: bstring -> class list -> Element.context_i list -> theory
   13.10 -    -> ProofContext.context * theory
   13.11 +    -> Proof.context * theory
   13.12    (*FIXME: in _i variants, bstring should be bstring option*)
   13.13    val instance_arity: ((xstring * string list) * string) list
   13.14      -> bstring * Attrib.src list -> ((bstring * Attrib.src list) * string) list
    14.1 --- a/src/Pure/meta_simplifier.ML	Wed Aug 02 22:26:40 2006 +0200
    14.2 +++ b/src/Pure/meta_simplifier.ML	Wed Aug 02 22:26:41 2006 +0200
    14.3 @@ -28,7 +28,7 @@
    14.4     {rules: rrule Net.net,
    14.5      prems: thm list,
    14.6      bounds: int * ((string * typ) * string) list,
    14.7 -    context: Context.proof option} *
    14.8 +    context: Proof.context option} *
    14.9     {congs: (string * cong) list * string list,
   14.10      procs: proc Net.net,
   14.11      mk_rews:
   14.12 @@ -88,8 +88,8 @@
   14.13    val simproc: theory -> string -> string list
   14.14      -> (theory -> simpset -> term -> thm option) -> simproc
   14.15    val inherit_context: simpset -> simpset -> simpset
   14.16 -  val the_context: simpset -> Context.proof
   14.17 -  val context: Context.proof -> simpset -> simpset
   14.18 +  val the_context: simpset -> Proof.context
   14.19 +  val context: Proof.context -> simpset -> simpset
   14.20    val theory_context: theory  -> simpset -> simpset
   14.21    val debug_bounds: bool ref
   14.22    val set_reorient: (theory -> term list -> term -> term -> bool) -> simpset -> simpset
   14.23 @@ -175,7 +175,7 @@
   14.24     {rules: rrule Net.net,
   14.25      prems: thm list,
   14.26      bounds: int * ((string * typ) * string) list,
   14.27 -    context: Context.proof option} *
   14.28 +    context: Proof.context option} *
   14.29     {congs: (string * cong) list * string list,
   14.30      procs: proc Net.net,
   14.31      mk_rews: mk_rews,
    15.1 --- a/src/Pure/thm.ML	Wed Aug 02 22:26:40 2006 +0200
    15.2 +++ b/src/Pure/thm.ML	Wed Aug 02 22:26:41 2006 +0200
    15.3 @@ -142,7 +142,7 @@
    15.4    val rule_attribute: (Context.generic -> thm -> thm) -> attribute
    15.5    val declaration_attribute: (thm -> Context.generic -> Context.generic) -> attribute
    15.6    val theory_attributes: attribute list -> theory * thm -> theory * thm
    15.7 -  val proof_attributes: attribute list -> Context.proof * thm -> Context.proof * thm
    15.8 +  val proof_attributes: attribute list -> Proof.context * thm -> Proof.context * thm
    15.9    val no_attributes: 'a -> 'a * 'b list
   15.10    val simple_fact: 'a -> ('a * 'b list) list
   15.11    val terms_of_tpairs: (term * term) list -> term list