--- 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
--- 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
--- 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
}
--- 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
-
-
-
-
-
-
-
-
-
-
--- 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
--- 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;
--- 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 =
--- 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 =
--- 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
--- 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,
--- 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 =
--- 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 =
--- 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
--- 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,
--- 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