--- a/doc-src/IsarImplementation/Thy/ML.thy Wed Jan 21 16:47:31 2009 +0100
+++ b/doc-src/IsarImplementation/Thy/ML.thy Wed Jan 21 16:47:32 2009 +0100
@@ -317,7 +317,7 @@
a theory by constant declararion and primitive definitions:
\smallskip\begin{mldecls}
- @{ML "Sign.declare_const: Properties.T -> (Binding.T * typ) * mixfix
+ @{ML "Sign.declare_const: Properties.T -> (binding * typ) * mixfix
-> theory -> term * theory"} \\
@{ML "Thm.add_def: bool -> bool -> bstring * term -> theory -> thm * theory"}
\end{mldecls}
--- a/doc-src/IsarImplementation/Thy/document/ML.tex Wed Jan 21 16:47:31 2009 +0100
+++ b/doc-src/IsarImplementation/Thy/document/ML.tex Wed Jan 21 16:47:32 2009 +0100
@@ -366,7 +366,7 @@
a theory by constant declararion and primitive definitions:
\smallskip\begin{mldecls}
- \verb|Sign.declare_const: Properties.T -> (Binding.T * typ) * mixfix|\isasep\isanewline%
+ \verb|Sign.declare_const: Properties.T -> (binding * typ) * mixfix|\isasep\isanewline%
\verb| -> theory -> term * theory| \\
\verb|Thm.add_def: bool -> bool -> bstring * term -> theory -> thm * theory|
\end{mldecls}
--- a/doc-src/IsarImplementation/Thy/document/logic.tex Wed Jan 21 16:47:31 2009 +0100
+++ b/doc-src/IsarImplementation/Thy/document/logic.tex Wed Jan 21 16:47:32 2009 +0100
@@ -325,9 +325,9 @@
\indexml{fastype\_of}\verb|fastype_of: term -> typ| \\
\indexml{lambda}\verb|lambda: term -> term -> term| \\
\indexml{betapply}\verb|betapply: term * term -> term| \\
- \indexml{Sign.declare\_const}\verb|Sign.declare_const: Properties.T -> (Binding.T * typ) * mixfix ->|\isasep\isanewline%
+ \indexml{Sign.declare\_const}\verb|Sign.declare_const: Properties.T -> (binding * typ) * mixfix ->|\isasep\isanewline%
\verb| theory -> term * theory| \\
- \indexml{Sign.add\_abbrev}\verb|Sign.add_abbrev: string -> Properties.T -> Binding.T * term ->|\isasep\isanewline%
+ \indexml{Sign.add\_abbrev}\verb|Sign.add_abbrev: string -> Properties.T -> binding * term ->|\isasep\isanewline%
\verb| theory -> (term * term) * theory| \\
\indexml{Sign.const\_typargs}\verb|Sign.const_typargs: theory -> string * typ -> typ list| \\
\indexml{Sign.const\_instance}\verb|Sign.const_instance: theory -> string * typ list -> typ| \\
--- a/doc-src/IsarImplementation/Thy/document/prelim.tex Wed Jan 21 16:47:31 2009 +0100
+++ b/doc-src/IsarImplementation/Thy/document/prelim.tex Wed Jan 21 16:47:32 2009 +0100
@@ -816,13 +816,13 @@
\indexmltype{NameSpace.naming}\verb|type NameSpace.naming| \\
\indexml{NameSpace.default\_naming}\verb|NameSpace.default_naming: NameSpace.naming| \\
\indexml{NameSpace.add\_path}\verb|NameSpace.add_path: string -> NameSpace.naming -> NameSpace.naming| \\
- \indexml{NameSpace.full\_name}\verb|NameSpace.full_name: NameSpace.naming -> Binding.T -> string| \\
+ \indexml{NameSpace.full\_name}\verb|NameSpace.full_name: NameSpace.naming -> binding -> string| \\
\end{mldecls}
\begin{mldecls}
\indexmltype{NameSpace.T}\verb|type NameSpace.T| \\
\indexml{NameSpace.empty}\verb|NameSpace.empty: NameSpace.T| \\
\indexml{NameSpace.merge}\verb|NameSpace.merge: NameSpace.T * NameSpace.T -> NameSpace.T| \\
- \indexml{NameSpace.declare}\verb|NameSpace.declare: NameSpace.naming -> Binding.T -> NameSpace.T -> string * NameSpace.T| \\
+ \indexml{NameSpace.declare}\verb|NameSpace.declare: NameSpace.naming -> binding -> NameSpace.T -> string * NameSpace.T| \\
\indexml{NameSpace.intern}\verb|NameSpace.intern: NameSpace.T -> string -> string| \\
\indexml{NameSpace.extern}\verb|NameSpace.extern: NameSpace.T -> string -> string| \\
\end{mldecls}
--- a/doc-src/IsarImplementation/Thy/logic.thy Wed Jan 21 16:47:31 2009 +0100
+++ b/doc-src/IsarImplementation/Thy/logic.thy Wed Jan 21 16:47:32 2009 +0100
@@ -323,9 +323,9 @@
@{index_ML fastype_of: "term -> typ"} \\
@{index_ML lambda: "term -> term -> term"} \\
@{index_ML betapply: "term * term -> term"} \\
- @{index_ML Sign.declare_const: "Properties.T -> (Binding.T * typ) * mixfix ->
+ @{index_ML Sign.declare_const: "Properties.T -> (binding * typ) * mixfix ->
theory -> term * theory"} \\
- @{index_ML Sign.add_abbrev: "string -> Properties.T -> Binding.T * term ->
+ @{index_ML Sign.add_abbrev: "string -> Properties.T -> binding * term ->
theory -> (term * term) * theory"} \\
@{index_ML Sign.const_typargs: "theory -> string * typ -> typ list"} \\
@{index_ML Sign.const_instance: "theory -> string * typ list -> typ"} \\
--- a/doc-src/IsarImplementation/Thy/prelim.thy Wed Jan 21 16:47:31 2009 +0100
+++ b/doc-src/IsarImplementation/Thy/prelim.thy Wed Jan 21 16:47:32 2009 +0100
@@ -707,13 +707,13 @@
@{index_ML_type NameSpace.naming} \\
@{index_ML NameSpace.default_naming: NameSpace.naming} \\
@{index_ML NameSpace.add_path: "string -> NameSpace.naming -> NameSpace.naming"} \\
- @{index_ML NameSpace.full_name: "NameSpace.naming -> Binding.T -> string"} \\
+ @{index_ML NameSpace.full_name: "NameSpace.naming -> binding -> string"} \\
\end{mldecls}
\begin{mldecls}
@{index_ML_type NameSpace.T} \\
@{index_ML NameSpace.empty: NameSpace.T} \\
@{index_ML NameSpace.merge: "NameSpace.T * NameSpace.T -> NameSpace.T"} \\
- @{index_ML NameSpace.declare: "NameSpace.naming -> Binding.T -> NameSpace.T -> string * NameSpace.T"} \\
+ @{index_ML NameSpace.declare: "NameSpace.naming -> binding -> NameSpace.T -> string * NameSpace.T"} \\
@{index_ML NameSpace.intern: "NameSpace.T -> string -> string"} \\
@{index_ML NameSpace.extern: "NameSpace.T -> string -> string"} \\
\end{mldecls}
--- a/src/HOL/Nominal/nominal_induct.ML Wed Jan 21 16:47:31 2009 +0100
+++ b/src/HOL/Nominal/nominal_induct.ML Wed Jan 21 16:47:32 2009 +0100
@@ -6,7 +6,7 @@
structure NominalInduct:
sig
- val nominal_induct_tac: Proof.context -> (Binding.T option * term) option list list ->
+ val nominal_induct_tac: Proof.context -> (binding option * term) option list list ->
(string * typ) list -> (string * typ) list list -> thm list ->
thm list -> int -> RuleCases.cases_tactic
val nominal_induct_method: Method.src -> Proof.context -> Method.method
--- a/src/HOL/Nominal/nominal_primrec.ML Wed Jan 21 16:47:31 2009 +0100
+++ b/src/HOL/Nominal/nominal_primrec.ML Wed Jan 21 16:47:32 2009 +0100
@@ -9,8 +9,8 @@
signature NOMINAL_PRIMREC =
sig
val add_primrec: term list option -> term option ->
- (Binding.T * typ option * mixfix) list ->
- (Binding.T * typ option * mixfix) list ->
+ (binding * typ option * mixfix) list ->
+ (binding * typ option * mixfix) list ->
(Attrib.binding * term) list -> local_theory -> Proof.state
end;
--- a/src/HOL/Tools/function_package/fundef_package.ML Wed Jan 21 16:47:31 2009 +0100
+++ b/src/HOL/Tools/function_package/fundef_package.ML Wed Jan 21 16:47:32 2009 +0100
@@ -9,14 +9,14 @@
signature FUNDEF_PACKAGE =
sig
- val add_fundef : (Binding.T * string option * mixfix) list
+ val add_fundef : (binding * string option * mixfix) list
-> (Attrib.binding * string) list
-> FundefCommon.fundef_config
-> bool list
-> local_theory
-> Proof.state
- val add_fundef_i: (Binding.T * typ option * mixfix) list
+ val add_fundef_i: (binding * typ option * mixfix) list
-> (Attrib.binding * term) list
-> FundefCommon.fundef_config
-> bool list
--- a/src/HOL/Tools/inductive_package.ML Wed Jan 21 16:47:31 2009 +0100
+++ b/src/HOL/Tools/inductive_package.ML Wed Jan 21 16:47:32 2009 +0100
@@ -38,17 +38,17 @@
thm list list * local_theory
type inductive_flags
val add_inductive_i:
- inductive_flags -> ((Binding.T * typ) * mixfix) list ->
+ inductive_flags -> ((binding * typ) * mixfix) list ->
(string * typ) list -> (Attrib.binding * term) list -> thm list -> local_theory ->
inductive_result * local_theory
val add_inductive: bool -> bool ->
- (Binding.T * string option * mixfix) list ->
- (Binding.T * string option * mixfix) list ->
+ (binding * string option * mixfix) list ->
+ (binding * string option * mixfix) list ->
(Attrib.binding * string) list ->
(Facts.ref * Attrib.src list) list ->
bool -> local_theory -> inductive_result * local_theory
val add_inductive_global: string -> inductive_flags ->
- ((Binding.T * typ) * mixfix) list -> (string * typ) list -> (Attrib.binding * term) list ->
+ ((binding * typ) * mixfix) list -> (string * typ) list -> (Attrib.binding * term) list ->
thm list -> theory -> inductive_result * theory
val arities_of: thm -> (string * int) list
val params_of: thm -> term list
@@ -63,16 +63,16 @@
sig
include BASIC_INDUCTIVE_PACKAGE
type add_ind_def
- val declare_rules: string -> Binding.T -> bool -> bool -> string list ->
- thm list -> Binding.T list -> Attrib.src list list -> (thm * string list) list ->
+ val declare_rules: string -> binding -> bool -> bool -> string list ->
+ thm list -> binding list -> Attrib.src list list -> (thm * string list) list ->
thm -> local_theory -> thm list * thm list * thm * local_theory
val add_ind_def: add_ind_def
val gen_add_inductive_i: add_ind_def -> inductive_flags ->
- ((Binding.T * typ) * mixfix) list -> (string * typ) list -> (Attrib.binding * term) list ->
+ ((binding * typ) * mixfix) list -> (string * typ) list -> (Attrib.binding * term) list ->
thm list -> local_theory -> inductive_result * local_theory
val gen_add_inductive: add_ind_def -> bool -> bool ->
- (Binding.T * string option * mixfix) list ->
- (Binding.T * string option * mixfix) list ->
+ (binding * string option * mixfix) list ->
+ (binding * string option * mixfix) list ->
(Attrib.binding * string) list -> (Facts.ref * Attrib.src list) list ->
bool -> local_theory -> inductive_result * local_theory
val gen_ind_decl: add_ind_def -> bool ->
@@ -720,13 +720,13 @@
in (intrs', elims', induct', ctxt3) end;
type inductive_flags =
- {quiet_mode: bool, verbose: bool, kind: string, alt_name: Binding.T,
+ {quiet_mode: bool, verbose: bool, kind: string, alt_name: binding,
coind: bool, no_elim: bool, no_ind: bool, skip_mono: bool, fork_mono: bool}
type add_ind_def =
inductive_flags ->
term list -> (Attrib.binding * term) list -> thm list ->
- term list -> (Binding.T * mixfix) list ->
+ term list -> (binding * mixfix) list ->
local_theory -> inductive_result * local_theory
fun add_ind_def {quiet_mode, verbose, kind, alt_name, coind, no_elim, no_ind, skip_mono, fork_mono}
--- a/src/HOL/Tools/inductive_set_package.ML Wed Jan 21 16:47:31 2009 +0100
+++ b/src/HOL/Tools/inductive_set_package.ML Wed Jan 21 16:47:32 2009 +0100
@@ -12,13 +12,13 @@
val pred_set_conv_att: attribute
val add_inductive_i:
InductivePackage.inductive_flags ->
- ((Binding.T * typ) * mixfix) list ->
+ ((binding * typ) * mixfix) list ->
(string * typ) list ->
(Attrib.binding * term) list -> thm list ->
local_theory -> InductivePackage.inductive_result * local_theory
val add_inductive: bool -> bool ->
- (Binding.T * string option * mixfix) list ->
- (Binding.T * string option * mixfix) list ->
+ (binding * string option * mixfix) list ->
+ (binding * string option * mixfix) list ->
(Attrib.binding * string) list -> (Facts.ref * Attrib.src list) list ->
bool -> local_theory -> InductivePackage.inductive_result * local_theory
val codegen_preproc: theory -> thm list -> thm list
--- a/src/HOL/Tools/primrec_package.ML Wed Jan 21 16:47:31 2009 +0100
+++ b/src/HOL/Tools/primrec_package.ML Wed Jan 21 16:47:32 2009 +0100
@@ -7,12 +7,12 @@
signature PRIMREC_PACKAGE =
sig
- val add_primrec: (Binding.T * typ option * mixfix) list ->
+ val add_primrec: (binding * typ option * mixfix) list ->
(Attrib.binding * term) list -> local_theory -> thm list * local_theory
- val add_primrec_global: (Binding.T * typ option * mixfix) list ->
+ val add_primrec_global: (binding * typ option * mixfix) list ->
(Attrib.binding * term) list -> theory -> thm list * theory
val add_primrec_overloaded: (string * (string * typ) * bool) list ->
- (Binding.T * typ option * mixfix) list ->
+ (binding * typ option * mixfix) list ->
(Attrib.binding * term) list -> theory -> thm list * theory
end;
--- a/src/HOLCF/Tools/fixrec_package.ML Wed Jan 21 16:47:31 2009 +0100
+++ b/src/HOLCF/Tools/fixrec_package.ML Wed Jan 21 16:47:32 2009 +0100
@@ -9,9 +9,9 @@
val legacy_infer_term: theory -> term -> term
val legacy_infer_prop: theory -> term -> term
val add_fixrec: bool -> (Attrib.binding * string) list list -> theory -> theory
- val add_fixrec_i: bool -> ((Binding.T * attribute list) * term) list list -> theory -> theory
+ val add_fixrec_i: bool -> ((binding * attribute list) * term) list list -> theory -> theory
val add_fixpat: Attrib.binding * string list -> theory -> theory
- val add_fixpat_i: (Binding.T * attribute list) * term list -> theory -> theory
+ val add_fixpat_i: (binding * attribute list) * term list -> theory -> theory
end;
structure FixrecPackage: FIXREC_PACKAGE =
--- a/src/Pure/General/binding.ML Wed Jan 21 16:47:31 2009 +0100
+++ b/src/Pure/General/binding.ML Wed Jan 21 16:47:32 2009 +0100
@@ -6,6 +6,7 @@
signature BASIC_BINDING =
sig
+ type binding
val long_names: bool ref
val short_names: bool ref
val unique_names: bool ref
@@ -92,6 +93,8 @@
else space_implode "." (map mk_prefix prefix) ^ ":" ^ name
end;
+type binding = T;
+
end;
structure Basic_Binding : BASIC_BINDING = Binding;
--- a/src/Pure/General/name_space.ML Wed Jan 21 16:47:31 2009 +0100
+++ b/src/Pure/General/name_space.ML Wed Jan 21 16:47:32 2009 +0100
@@ -3,9 +3,10 @@
Generic name spaces with declared and hidden entries. Unknown names
are considered global; no support for absolute addressing.
+Cf. Pure/General/binding.ML
*)
-type bstring = string; (*names to be bound*)
+type bstring = string; (*simple names to be bound -- legacy*)
type xstring = string; (*external names*)
signature NAME_SPACE =
@@ -31,8 +32,8 @@
val merge: T * T -> T
type naming
val default_naming: naming
- val declare: naming -> Binding.T -> T -> string * T
- val full_name: naming -> Binding.T -> string
+ val declare: naming -> binding -> T -> string * T
+ val full_name: naming -> binding -> string
val external_names: naming -> string -> string list
val path_of: naming -> string
val add_path: string -> naming -> naming
@@ -41,7 +42,7 @@
val sticky_prefix: string -> naming -> naming
type 'a table = T * 'a Symtab.table
val empty_table: 'a table
- val bind: naming -> Binding.T * 'a
+ val bind: naming -> binding * 'a
-> 'a table -> string * 'a table (*exception Symtab.DUP*)
val merge_tables: ('a * 'a -> bool) -> 'a table * 'a table -> 'a table
val join_tables: (string -> 'a * 'a -> 'a)
--- a/src/Pure/Isar/args.ML Wed Jan 21 16:47:31 2009 +0100
+++ b/src/Pure/Isar/args.ML Wed Jan 21 16:47:32 2009 +0100
@@ -35,7 +35,7 @@
val name_source: T list -> string * T list
val name_source_position: T list -> (SymbolPos.text * Position.T) * T list
val name: T list -> string * T list
- val binding: T list -> Binding.T * T list
+ val binding: T list -> binding * T list
val alt_name: T list -> string * T list
val symbol: T list -> string * T list
val liberal_name: T list -> string * T list
@@ -66,8 +66,8 @@
val parse1: (string -> bool) -> OuterLex.token list -> T list * OuterLex.token list
val attribs: (string -> string) -> T list -> src list * T list
val opt_attribs: (string -> string) -> T list -> src list * T list
- val thm_name: (string -> string) -> string -> T list -> (Binding.T * src list) * T list
- val opt_thm_name: (string -> string) -> string -> T list -> (Binding.T * src list) * T list
+ val thm_name: (string -> string) -> string -> T list -> (binding * src list) * T list
+ val opt_thm_name: (string -> string) -> string -> T list -> (binding * src list) * T list
val syntax: string -> ('b * T list -> 'a * ('b * T list)) -> src -> 'b -> 'a * 'b
val context_syntax: string -> (Context.generic * T list -> 'a * (Context.generic * T list)) ->
src -> Proof.context -> 'a * Proof.context
--- a/src/Pure/Isar/attrib.ML Wed Jan 21 16:47:31 2009 +0100
+++ b/src/Pure/Isar/attrib.ML Wed Jan 21 16:47:32 2009 +0100
@@ -7,7 +7,7 @@
signature ATTRIB =
sig
type src = Args.src
- type binding = Binding.T * src list
+ type binding = binding * src list
val empty_binding: binding
val print_attributes: theory -> unit
val intern: theory -> xstring -> string
@@ -54,7 +54,7 @@
type src = Args.src;
-type binding = Binding.T * src list;
+type binding = binding * src list;
val empty_binding: binding = (Binding.empty, []);
--- a/src/Pure/Isar/local_defs.ML Wed Jan 21 16:47:31 2009 +0100
+++ b/src/Pure/Isar/local_defs.ML Wed Jan 21 16:47:32 2009 +0100
@@ -11,10 +11,10 @@
val mk_def: Proof.context -> (string * term) list -> term list
val expand: cterm list -> thm -> thm
val def_export: Assumption.export
- val add_defs: ((Binding.T * mixfix) * ((Binding.T * attribute list) * term)) list ->
+ val add_defs: ((binding * mixfix) * ((binding * attribute list) * term)) list ->
Proof.context -> (term * (string * thm)) list * Proof.context
- val add_def: (Binding.T * mixfix) * term -> Proof.context -> (term * thm) * Proof.context
- val fixed_abbrev: (Binding.T * mixfix) * term -> Proof.context ->
+ val add_def: (binding * mixfix) * term -> Proof.context -> (term * thm) * Proof.context
+ val fixed_abbrev: (binding * mixfix) * term -> Proof.context ->
(term * term) * Proof.context
val export: Proof.context -> Proof.context -> thm -> thm list * thm
val export_cterm: Proof.context -> Proof.context -> cterm -> cterm * thm
--- a/src/Pure/Isar/local_theory.ML Wed Jan 21 16:47:31 2009 +0100
+++ b/src/Pure/Isar/local_theory.ML Wed Jan 21 16:47:32 2009 +0100
@@ -18,16 +18,16 @@
val raw_theory: (theory -> theory) -> local_theory -> local_theory
val checkpoint: local_theory -> local_theory
val full_naming: local_theory -> NameSpace.naming
- val full_name: local_theory -> Binding.T -> string
+ val full_name: local_theory -> binding -> string
val theory_result: (theory -> 'a * theory) -> local_theory -> 'a * local_theory
val theory: (theory -> theory) -> local_theory -> local_theory
val target_result: (Proof.context -> 'a * Proof.context) -> local_theory -> 'a * local_theory
val target: (Proof.context -> Proof.context) -> local_theory -> local_theory
val affirm: local_theory -> local_theory
val pretty: local_theory -> Pretty.T list
- val abbrev: Syntax.mode -> (Binding.T * mixfix) * term -> local_theory ->
+ val abbrev: Syntax.mode -> (binding * mixfix) * term -> local_theory ->
(term * term) * local_theory
- val define: string -> (Binding.T * mixfix) * (Attrib.binding * term) -> local_theory ->
+ val define: string -> (binding * mixfix) * (Attrib.binding * term) -> local_theory ->
(term * (string * thm)) * local_theory
val note: string -> Attrib.binding * thm list -> local_theory -> (string * thm list) * local_theory
val notes: string -> (Attrib.binding * (thm list * Attrib.src list) list) list ->
@@ -55,10 +55,10 @@
type operations =
{pretty: local_theory -> Pretty.T list,
- abbrev: Syntax.mode -> (Binding.T * mixfix) * term -> local_theory ->
+ abbrev: Syntax.mode -> (binding * mixfix) * term -> local_theory ->
(term * term) * local_theory,
define: string ->
- (Binding.T * mixfix) * (Attrib.binding * term) -> local_theory ->
+ (binding * mixfix) * (Attrib.binding * term) -> local_theory ->
(term * (string * thm)) * local_theory,
notes: string ->
(Attrib.binding * (thm list * Attrib.src list) list) list ->
--- a/src/Pure/Isar/obtain.ML Wed Jan 21 16:47:31 2009 +0100
+++ b/src/Pure/Isar/obtain.ML Wed Jan 21 16:47:32 2009 +0100
@@ -39,16 +39,16 @@
signature OBTAIN =
sig
val thatN: string
- val obtain: string -> (Binding.T * string option * mixfix) list ->
+ val obtain: string -> (binding * string option * mixfix) list ->
(Attrib.binding * (string * string list) list) list ->
bool -> Proof.state -> Proof.state
- val obtain_i: string -> (Binding.T * typ option * mixfix) list ->
- ((Binding.T * attribute list) * (term * term list) list) list ->
+ val obtain_i: string -> (binding * typ option * mixfix) list ->
+ ((binding * attribute list) * (term * term list) list) list ->
bool -> Proof.state -> Proof.state
val result: (Proof.context -> tactic) -> thm list -> Proof.context ->
(cterm list * thm list) * Proof.context
- val guess: (Binding.T * string option * mixfix) list -> bool -> Proof.state -> Proof.state
- val guess_i: (Binding.T * typ option * mixfix) list -> bool -> Proof.state -> Proof.state
+ val guess: (binding * string option * mixfix) list -> bool -> Proof.state -> Proof.state
+ val guess_i: (binding * typ option * mixfix) list -> bool -> Proof.state -> Proof.state
end;
structure Obtain: OBTAIN =
--- a/src/Pure/Isar/outer_parse.ML Wed Jan 21 16:47:31 2009 +0100
+++ b/src/Pure/Isar/outer_parse.ML Wed Jan 21 16:47:32 2009 +0100
@@ -61,12 +61,12 @@
val list: 'a parser -> 'a list parser
val list1: 'a parser -> 'a list parser
val name: bstring parser
- val binding: Binding.T parser
+ val binding: binding parser
val xname: xstring parser
val text: string parser
val path: Path.T parser
val parname: string parser
- val parbinding: Binding.T parser
+ val parbinding: binding parser
val sort: string parser
val arity: (string * string list * string) parser
val multi_arity: (string list * string list * string) parser
@@ -81,11 +81,11 @@
val opt_mixfix': mixfix parser
val where_: string parser
val const: (string * string * mixfix) parser
- val params: (Binding.T * string option) list parser
- val simple_fixes: (Binding.T * string option) list parser
- val fixes: (Binding.T * string option * mixfix) list parser
- val for_fixes: (Binding.T * string option * mixfix) list parser
- val for_simple_fixes: (Binding.T * string option) list parser
+ val params: (binding * string option) list parser
+ val simple_fixes: (binding * string option) list parser
+ val fixes: (binding * string option * mixfix) list parser
+ val for_fixes: (binding * string option * mixfix) list parser
+ val for_simple_fixes: (binding * string option) list parser
val ML_source: (SymbolPos.text * Position.T) parser
val doc_source: (SymbolPos.text * Position.T) parser
val term_group: string parser
--- a/src/Pure/Isar/proof.ML Wed Jan 21 16:47:31 2009 +0100
+++ b/src/Pure/Isar/proof.ML Wed Jan 21 16:47:32 2009 +0100
@@ -43,27 +43,27 @@
val match_bind_i: (term list * term) list -> state -> state
val let_bind: (string list * string) list -> state -> state
val let_bind_i: (term list * term) list -> state -> state
- val fix: (Binding.T * string option * mixfix) list -> state -> state
- val fix_i: (Binding.T * typ option * mixfix) list -> state -> state
+ val fix: (binding * string option * mixfix) list -> state -> state
+ val fix_i: (binding * typ option * mixfix) list -> state -> state
val assm: Assumption.export ->
(Attrib.binding * (string * string list) list) list -> state -> state
val assm_i: Assumption.export ->
- ((Binding.T * attribute list) * (term * term list) list) list -> state -> state
+ ((binding * attribute list) * (term * term list) list) list -> state -> state
val assume: (Attrib.binding * (string * string list) list) list -> state -> state
- val assume_i: ((Binding.T * attribute list) * (term * term list) list) list ->
+ val assume_i: ((binding * attribute list) * (term * term list) list) list ->
state -> state
val presume: (Attrib.binding * (string * string list) list) list -> state -> state
- val presume_i: ((Binding.T * attribute list) * (term * term list) list) list ->
+ val presume_i: ((binding * attribute list) * (term * term list) list) list ->
state -> state
- val def: (Attrib.binding * ((Binding.T * mixfix) * (string * string list))) list ->
+ val def: (Attrib.binding * ((binding * mixfix) * (string * string list))) list ->
state -> state
- val def_i: ((Binding.T * attribute list) *
- ((Binding.T * mixfix) * (term * term list))) list -> state -> state
+ val def_i: ((binding * attribute list) *
+ ((binding * mixfix) * (term * term list))) list -> state -> state
val chain: state -> state
val chain_facts: thm list -> state -> state
val get_thmss: state -> (Facts.ref * Attrib.src list) list -> thm list
val note_thmss: (Attrib.binding * (Facts.ref * Attrib.src list) list) list -> state -> state
- val note_thmss_i: ((Binding.T * attribute list) *
+ val note_thmss_i: ((binding * attribute list) *
(thm list * attribute list) list) list -> state -> state
val from_thmss: ((Facts.ref * Attrib.src list) list) list -> state -> state
val from_thmss_i: ((thm list * attribute list) list) list -> state -> state
@@ -87,7 +87,7 @@
(theory -> 'a -> attribute) ->
(context * 'b list -> context * (term list list * (context -> context))) ->
string -> Method.text option -> (thm list list -> state -> state) ->
- ((Binding.T * 'a list) * 'b) list -> state -> state
+ ((binding * 'a list) * 'b) list -> state -> state
val local_qed: Method.text option * bool -> state -> state
val theorem: Method.text option -> (thm list list -> context -> context) ->
(string * string list) list list -> context -> state
@@ -107,11 +107,11 @@
val have: Method.text option -> (thm list list -> state -> state) ->
(Attrib.binding * (string * string list) list) list -> bool -> state -> state
val have_i: Method.text option -> (thm list list -> state -> state) ->
- ((Binding.T * attribute list) * (term * term list) list) list -> bool -> state -> state
+ ((binding * attribute list) * (term * term list) list) list -> bool -> state -> state
val show: Method.text option -> (thm list list -> state -> state) ->
(Attrib.binding * (string * string list) list) list -> bool -> state -> state
val show_i: Method.text option -> (thm list list -> state -> state) ->
- ((Binding.T * attribute list) * (term * term list) list) list -> bool -> state -> state
+ ((binding * attribute list) * (term * term list) list) list -> bool -> state -> state
val schematic_goal: state -> bool
val is_relevant: state -> bool
val local_future_proof: (state -> ('a * state) Future.future) ->
--- a/src/Pure/Isar/proof_context.ML Wed Jan 21 16:47:31 2009 +0100
+++ b/src/Pure/Isar/proof_context.ML Wed Jan 21 16:47:32 2009 +0100
@@ -23,7 +23,7 @@
val abbrev_mode: Proof.context -> bool
val set_stmt: bool -> Proof.context -> Proof.context
val naming_of: Proof.context -> NameSpace.naming
- val full_name: Proof.context -> Binding.T -> string
+ val full_name: Proof.context -> binding -> string
val full_bname: Proof.context -> bstring -> string
val consts_of: Proof.context -> Consts.T
val const_syntax_name: Proof.context -> string -> string
@@ -105,27 +105,27 @@
val restore_naming: Proof.context -> Proof.context -> Proof.context
val reset_naming: Proof.context -> Proof.context
val note_thmss: string ->
- ((Binding.T * attribute list) * (Facts.ref * attribute list) list) list ->
+ ((binding * attribute list) * (Facts.ref * attribute list) list) list ->
Proof.context -> (string * thm list) list * Proof.context
val note_thmss_i: string ->
- ((Binding.T * attribute list) * (thm list * attribute list) list) list ->
+ ((binding * attribute list) * (thm list * attribute list) list) list ->
Proof.context -> (string * thm list) list * Proof.context
val put_thms: bool -> string * thm list option -> Proof.context -> Proof.context
- val read_vars: (Binding.T * string option * mixfix) list -> Proof.context ->
- (Binding.T * typ option * mixfix) list * Proof.context
- val cert_vars: (Binding.T * typ option * mixfix) list -> Proof.context ->
- (Binding.T * typ option * mixfix) list * Proof.context
- val add_fixes: (Binding.T * string option * mixfix) list ->
+ val read_vars: (binding * string option * mixfix) list -> Proof.context ->
+ (binding * typ option * mixfix) list * Proof.context
+ val cert_vars: (binding * typ option * mixfix) list -> Proof.context ->
+ (binding * typ option * mixfix) list * Proof.context
+ val add_fixes: (binding * string option * mixfix) list ->
Proof.context -> string list * Proof.context
- val add_fixes_i: (Binding.T * typ option * mixfix) list ->
+ val add_fixes_i: (binding * typ option * mixfix) list ->
Proof.context -> string list * Proof.context
val auto_fixes: Proof.context * (term list list * 'a) -> Proof.context * (term list list * 'a)
val bind_fixes: string list -> Proof.context -> (term -> term) * Proof.context
val add_assms: Assumption.export ->
- ((Binding.T * attribute list) * (string * string list) list) list ->
+ ((binding * attribute list) * (string * string list) list) list ->
Proof.context -> (string * thm list) list * Proof.context
val add_assms_i: Assumption.export ->
- ((Binding.T * attribute list) * (term * term list) list) list ->
+ ((binding * attribute list) * (term * term list) list) list ->
Proof.context -> (string * thm list) list * Proof.context
val add_cases: bool -> (string * RuleCases.T option) list -> Proof.context -> Proof.context
val apply_case: RuleCases.T -> Proof.context -> (string * term list) list * Proof.context
@@ -135,7 +135,7 @@
Context.generic -> Context.generic
val add_const_constraint: string * typ option -> Proof.context -> Proof.context
val add_abbrev: string -> Properties.T ->
- Binding.T * term -> Proof.context -> (term * term) * Proof.context
+ binding * term -> Proof.context -> (term * term) * Proof.context
val revert_abbrev: string -> string -> Proof.context -> Proof.context
val verbose: bool ref
val setmp_verbose: ('a -> 'b) -> 'a -> 'b
--- a/src/Pure/Isar/spec_parse.ML Wed Jan 21 16:47:31 2009 +0100
+++ b/src/Pure/Isar/spec_parse.ML Wed Jan 21 16:47:32 2009 +0100
@@ -15,24 +15,23 @@
val opt_thm_name: string -> Attrib.binding parser
val spec: (Attrib.binding * string list) parser
val named_spec: (Attrib.binding * string list) parser
- val spec_name: ((Binding.T * string) * Attrib.src list) parser
- val spec_opt_name: ((Binding.T * string) * Attrib.src list) parser
+ val spec_name: ((binding * string) * Attrib.src list) parser
+ val spec_opt_name: ((binding * string) * Attrib.src list) parser
val xthm: (Facts.ref * Attrib.src list) parser
val xthms1: (Facts.ref * Attrib.src list) list parser
val name_facts: (Attrib.binding * (Facts.ref * Attrib.src list) list) list parser
val locale_mixfix: mixfix parser
- val locale_fixes: (Binding.T * string option * mixfix) list parser
+ val locale_fixes: (binding * string option * mixfix) list parser
val locale_insts: (string option list * (Attrib.binding * string) list) parser
val class_expr: string list parser
- val locale_expr: Old_Locale.expr parser
- val locale_expression: Expression.expression parser
+ val locale_expression: Expression.expression parser
val locale_keyword: string parser
val context_element: Element.context parser
val statement: (Attrib.binding * (string * string list) list) list parser
val general_statement: (Element.context list * Element.statement) parser
val statement_keyword: string parser
val specification:
- (Binding.T * ((Attrib.binding * string list) list * (Binding.T * string option) list)) list parser
+ (binding * ((Attrib.binding * string list) list * (binding * string option) list)) list parser
end;
structure SpecParse: SPEC_PARSE =
@@ -115,13 +114,6 @@
val class_expr = plus1_unless locale_keyword P.xname;
-val locale_expr =
- let
- fun expr2 x = (P.xname >> Old_Locale.Locale || P.$$$ "(" |-- P.!!! (expr0 --| P.$$$ ")")) x
- and expr1 x = (expr2 -- Scan.repeat1 (P.maybe rename) >> Old_Locale.Rename || expr2) x
- and expr0 x = (plus1_unless locale_keyword expr1 >> (fn [e] => e | es => Old_Locale.Merge es)) x;
- in expr0 end;
-
val locale_expression =
let
fun expr2 x = P.xname x;
--- a/src/Pure/Isar/specification.ML Wed Jan 21 16:47:31 2009 +0100
+++ b/src/Pure/Isar/specification.ML Wed Jan 21 16:47:32 2009 +0100
@@ -9,33 +9,33 @@
signature SPECIFICATION =
sig
val print_consts: local_theory -> (string * typ -> bool) -> (string * typ) list -> unit
- val check_specification: (Binding.T * typ option * mixfix) list ->
+ val check_specification: (binding * typ option * mixfix) list ->
(Attrib.binding * term list) list list -> Proof.context ->
- (((Binding.T * typ) * mixfix) list * (Attrib.binding * term list) list) * Proof.context
- val read_specification: (Binding.T * string option * mixfix) list ->
+ (((binding * typ) * mixfix) list * (Attrib.binding * term list) list) * Proof.context
+ val read_specification: (binding * string option * mixfix) list ->
(Attrib.binding * string list) list list -> Proof.context ->
- (((Binding.T * typ) * mixfix) list * (Attrib.binding * term list) list) * Proof.context
- val check_free_specification: (Binding.T * typ option * mixfix) list ->
+ (((binding * typ) * mixfix) list * (Attrib.binding * term list) list) * Proof.context
+ val check_free_specification: (binding * typ option * mixfix) list ->
(Attrib.binding * term list) list -> Proof.context ->
- (((Binding.T * typ) * mixfix) list * (Attrib.binding * term list) list) * Proof.context
- val read_free_specification: (Binding.T * string option * mixfix) list ->
+ (((binding * typ) * mixfix) list * (Attrib.binding * term list) list) * Proof.context
+ val read_free_specification: (binding * string option * mixfix) list ->
(Attrib.binding * string list) list -> Proof.context ->
- (((Binding.T * typ) * mixfix) list * (Attrib.binding * term list) list) * Proof.context
- val axiomatization: (Binding.T * typ option * mixfix) list ->
+ (((binding * typ) * mixfix) list * (Attrib.binding * term list) list) * Proof.context
+ val axiomatization: (binding * typ option * mixfix) list ->
(Attrib.binding * term list) list -> theory ->
(term list * (string * thm list) list) * theory
- val axiomatization_cmd: (Binding.T * string option * mixfix) list ->
+ val axiomatization_cmd: (binding * string option * mixfix) list ->
(Attrib.binding * string list) list -> theory ->
(term list * (string * thm list) list) * theory
val definition:
- (Binding.T * typ option * mixfix) option * (Attrib.binding * term) ->
+ (binding * typ option * mixfix) option * (Attrib.binding * term) ->
local_theory -> (term * (string * thm)) * local_theory
val definition_cmd:
- (Binding.T * string option * mixfix) option * (Attrib.binding * string) ->
+ (binding * string option * mixfix) option * (Attrib.binding * string) ->
local_theory -> (term * (string * thm)) * local_theory
- val abbreviation: Syntax.mode -> (Binding.T * typ option * mixfix) option * term ->
+ val abbreviation: Syntax.mode -> (binding * typ option * mixfix) option * term ->
local_theory -> local_theory
- val abbreviation_cmd: Syntax.mode -> (Binding.T * string option * mixfix) option * string ->
+ val abbreviation_cmd: Syntax.mode -> (binding * string option * mixfix) option * string ->
local_theory -> local_theory
val notation: bool -> Syntax.mode -> (term * mixfix) list -> local_theory -> local_theory
val notation_cmd: bool -> Syntax.mode -> (string * mixfix) list -> local_theory -> local_theory
@@ -149,7 +149,8 @@
(*axioms*)
val (axioms, axioms_thy) = consts_thy |> fold_map (fn ((b, atts), props) =>
- fold_map Thm.add_axiom (PureThy.name_multi (Binding.base_name b) (map subst props))
+ fold_map Thm.add_axiom
+ ((map o apfst) Binding.name (PureThy.name_multi (Binding.base_name b) (map subst props)))
#>> (fn ths => ((b, atts), [(map Drule.standard' ths, [])]))) specs;
val (facts, thy') = axioms_thy |> PureThy.note_thmss Thm.axiomK
(Attrib.map_facts (Attrib.attribute_i axioms_thy) axioms);
--- a/src/Pure/consts.ML Wed Jan 21 16:47:31 2009 +0100
+++ b/src/Pure/consts.ML Wed Jan 21 16:47:32 2009 +0100
@@ -30,10 +30,10 @@
val certify: Pretty.pp -> Type.tsig -> bool -> T -> term -> term (*exception TYPE*)
val typargs: T -> string * typ -> typ list
val instance: T -> string * typ list -> typ
- val declare: bool -> NameSpace.naming -> Properties.T -> (Binding.T * typ) -> T -> T
+ val declare: bool -> NameSpace.naming -> Properties.T -> (binding * typ) -> T -> T
val constrain: string * typ option -> T -> T
val abbreviate: Pretty.pp -> Type.tsig -> NameSpace.naming -> string -> Properties.T ->
- Binding.T * term -> T -> (term * term) * T
+ binding * term -> T -> (term * term) * T
val revert_abbrev: string -> string -> T -> T
val hide: bool -> string -> T -> T
val empty: T
--- a/src/Pure/facts.ML Wed Jan 21 16:47:31 2009 +0100
+++ b/src/Pure/facts.ML Wed Jan 21 16:47:32 2009 +0100
@@ -30,9 +30,9 @@
val props: T -> thm list
val could_unify: T -> term -> thm list
val merge: T * T -> T
- val add_global: NameSpace.naming -> Binding.T * thm list -> T -> string * T
- val add_local: bool -> NameSpace.naming -> Binding.T * thm list -> T -> string * T
- val add_dynamic: NameSpace.naming -> Binding.T * (Context.generic -> thm list) -> T -> string * T
+ val add_global: NameSpace.naming -> binding * thm list -> T -> string * T
+ val add_local: bool -> NameSpace.naming -> binding * thm list -> T -> string * T
+ val add_dynamic: NameSpace.naming -> binding * (Context.generic -> thm list) -> T -> string * T
val del: string -> T -> T
val hide: bool -> string -> T -> T
end;
--- a/src/Pure/morphism.ML Wed Jan 21 16:47:31 2009 +0100
+++ b/src/Pure/morphism.ML Wed Jan 21 16:47:32 2009 +0100
@@ -16,21 +16,21 @@
signature MORPHISM =
sig
include BASIC_MORPHISM
- val var: morphism -> Binding.T * mixfix -> Binding.T * mixfix
- val binding: morphism -> Binding.T -> Binding.T
+ val var: morphism -> binding * mixfix -> binding * mixfix
+ val binding: morphism -> binding -> binding
val typ: morphism -> typ -> typ
val term: morphism -> term -> term
val fact: morphism -> thm list -> thm list
val thm: morphism -> thm -> thm
val cterm: morphism -> cterm -> cterm
val morphism:
- {binding: Binding.T -> Binding.T,
- var: Binding.T * mixfix -> Binding.T * mixfix,
+ {binding: binding -> binding,
+ var: binding * mixfix -> binding * mixfix,
typ: typ -> typ,
term: term -> term,
fact: thm list -> thm list} -> morphism
- val binding_morphism: (Binding.T -> Binding.T) -> morphism
- val var_morphism: (Binding.T * mixfix -> Binding.T * mixfix) -> morphism
+ val binding_morphism: (binding -> binding) -> morphism
+ val var_morphism: (binding * mixfix -> binding * mixfix) -> morphism
val typ_morphism: (typ -> typ) -> morphism
val term_morphism: (term -> term) -> morphism
val fact_morphism: (thm list -> thm list) -> morphism
@@ -45,8 +45,8 @@
struct
datatype morphism = Morphism of
- {binding: Binding.T -> Binding.T,
- var: Binding.T * mixfix -> Binding.T * mixfix,
+ {binding: binding -> binding,
+ var: binding * mixfix -> binding * mixfix,
typ: typ -> typ,
term: term -> term,
fact: thm list -> thm list};
--- a/src/Pure/sign.ML Wed Jan 21 16:47:31 2009 +0100
+++ b/src/Pure/sign.ML Wed Jan 21 16:47:32 2009 +0100
@@ -14,7 +14,7 @@
tsig: Type.tsig,
consts: Consts.T}
val naming_of: theory -> NameSpace.naming
- val full_name: theory -> Binding.T -> string
+ val full_name: theory -> binding -> string
val base_name: string -> bstring
val full_bname: theory -> bstring -> string
val full_bname_path: theory -> string -> bstring -> string
@@ -91,10 +91,10 @@
val del_modesyntax: Syntax.mode -> (bstring * string * mixfix) list -> theory -> theory
val del_modesyntax_i: Syntax.mode -> (bstring * typ * mixfix) list -> theory -> theory
val notation: bool -> Syntax.mode -> (term * mixfix) list -> theory -> theory
- val declare_const: Properties.T -> (Binding.T * typ) * mixfix -> theory -> term * theory
+ val declare_const: Properties.T -> (binding * typ) * mixfix -> theory -> term * theory
val add_consts: (bstring * string * mixfix) list -> theory -> theory
val add_consts_i: (bstring * typ * mixfix) list -> theory -> theory
- val add_abbrev: string -> Properties.T -> Binding.T * term -> theory -> (term * term) * theory
+ val add_abbrev: string -> Properties.T -> binding * term -> theory -> (term * term) * theory
val revert_abbrev: string -> string -> theory -> theory
val add_const_constraint: string * typ option -> theory -> theory
val primitive_class: string * class list -> theory -> theory
--- a/src/Pure/theory.ML Wed Jan 21 16:47:31 2009 +0100
+++ b/src/Pure/theory.ML Wed Jan 21 16:47:32 2009 +0100
@@ -29,14 +29,14 @@
val at_end: (theory -> theory option) -> theory -> theory
val begin_theory: string -> theory list -> theory
val end_theory: theory -> theory
+ val add_axioms_i: (binding * term) list -> theory -> theory
val add_axioms: (bstring * string) list -> theory -> theory
- val add_axioms_i: (bstring * term) list -> theory -> theory
val add_deps: string -> string * typ -> (string * typ) list -> theory -> theory
+ val add_defs_i: bool -> bool -> (binding * term) list -> theory -> theory
val add_defs: bool -> bool -> (bstring * string) list -> theory -> theory
- val add_defs_i: bool -> bool -> (bstring * term) list -> theory -> theory
+ val add_finals_i: bool -> term list -> theory -> theory
val add_finals: bool -> string list -> theory -> theory
- val add_finals_i: bool -> term list -> theory -> theory
- val specify_const: Properties.T -> (Binding.T * typ) * mixfix -> theory -> term * theory
+ val specify_const: Properties.T -> (binding * typ) * mixfix -> theory -> term * theory
end
structure Theory: THEORY =
@@ -157,19 +157,19 @@
fun err_in_axm msg name =
cat_error msg ("The error(s) above occurred in axiom " ^ quote name);
-fun cert_axm thy (name, raw_tm) =
+fun cert_axm thy (b, raw_tm) =
let
val (t, T, _) = Sign.certify_prop thy raw_tm
handle TYPE (msg, _, _) => error msg
| TERM (msg, _) => error msg;
in
Term.no_dummy_patterns t handle TERM (msg, _) => error msg;
- (name, Sign.no_vars (Syntax.pp_global thy) t)
+ (b, Sign.no_vars (Syntax.pp_global thy) t)
end;
-fun read_axm thy (name, str) =
- cert_axm thy (name, Syntax.read_prop_global thy str)
- handle ERROR msg => err_in_axm msg name;
+fun read_axm thy (bname, str) =
+ cert_axm thy (Binding.name bname, Syntax.read_prop_global thy str)
+ handle ERROR msg => err_in_axm msg bname;
(* add_axioms(_i) *)
@@ -178,15 +178,15 @@
fun gen_add_axioms prep_axm raw_axms thy = thy |> map_axioms (fn axioms =>
let
- val axms = map (apfst Binding.name o apsnd Logic.varify o prep_axm thy) raw_axms;
+ val axms = map (apsnd Logic.varify o prep_axm thy) raw_axms;
val axioms' = fold (snd oo NameSpace.bind (Sign.naming_of thy)) axms axioms
handle Symtab.DUP dup => err_dup_axm dup;
in axioms' end);
in
+val add_axioms_i = gen_add_axioms cert_axm;
val add_axioms = gen_add_axioms read_axm;
-val add_axioms_i = gen_add_axioms cert_axm;
end;
@@ -250,16 +250,16 @@
(* check_def *)
-fun check_def thy unchecked overloaded (bname, tm) defs =
+fun check_def thy unchecked overloaded (b, tm) defs =
let
val ctxt = ProofContext.init thy;
- val name = Sign.full_bname thy bname;
+ val name = Sign.full_name thy b;
val (lhs_const, rhs) = Sign.cert_def ctxt tm;
val rhs_consts = fold_aterms (fn Const const => insert (op =) const | _ => I) rhs [];
val _ = check_overloading thy overloaded lhs_const;
in defs |> dependencies thy unchecked true name lhs_const rhs_consts end
handle ERROR msg => cat_error msg (Pretty.string_of (Pretty.block
- [Pretty.str ("The error(s) above occurred in definition " ^ quote bname ^ ":"),
+ [Pretty.str ("The error(s) above occurred in definition " ^ quote (Binding.display b) ^ ":"),
Pretty.fbrk, Pretty.quote (Syntax.pretty_term_global thy tm)]));
@@ -298,8 +298,8 @@
in
+val add_finals_i = gen_add_finals (K I);
val add_finals = gen_add_finals Syntax.read_term_global;
-val add_finals_i = gen_add_finals (K I);
end;
--- a/src/Tools/induct.ML Wed Jan 21 16:47:31 2009 +0100
+++ b/src/Tools/induct.ML Wed Jan 21 16:47:32 2009 +0100
@@ -50,7 +50,7 @@
val setN: string
(*proof methods*)
val fix_tac: Proof.context -> int -> (string * typ) list -> int -> tactic
- val add_defs: (Binding.T option * term) option list -> Proof.context ->
+ val add_defs: (binding option * term) option list -> Proof.context ->
(term option list * thm list) * Proof.context
val atomize_term: theory -> term -> term
val atomize_tac: int -> tactic
@@ -62,7 +62,7 @@
val cases_tac: Proof.context -> term option list list -> thm option ->
thm list -> int -> cases_tactic
val get_inductT: Proof.context -> term option list list -> thm list list
- val induct_tac: Proof.context -> (Binding.T option * term) option list list ->
+ val induct_tac: Proof.context -> (binding option * term) option list list ->
(string * typ) list list -> term option list -> thm list option ->
thm list -> int -> cases_tactic
val coinduct_tac: Proof.context -> term option list -> term option list -> thm option ->