--- a/doc-src/IsarRef/Thy/Misc.thy Sun Nov 08 15:45:09 2009 +0100
+++ b/doc-src/IsarRef/Thy/Misc.thy Sun Nov 08 20:50:31 2009 +0100
@@ -21,7 +21,7 @@
\end{matharray}
\begin{rail}
- 'print\_theory' ( '!'?)
+ ('print\_theory' | 'print\_theorems') ('!'?)
;
'find\_theorems' (('(' (nat)? ('with\_dups')? ')')?) (thmcriterion *)
@@ -56,8 +56,8 @@
\item @{command "print_attributes"} prints all attributes
available in the current theory context.
- \item @{command "print_theorems"} prints theorems resulting from
- the last command.
+ \item @{command "print_theorems"} prints theorems resulting from the
+ last command; the ``@{text "!"}'' option indicates extra verbosity.
\item @{command "find_theorems"}~@{text criteria} retrieves facts
from the theory or proof context matching all of given search
--- a/doc-src/IsarRef/Thy/Spec.thy Sun Nov 08 15:45:09 2009 +0100
+++ b/doc-src/IsarRef/Thy/Spec.thy Sun Nov 08 20:50:31 2009 +0100
@@ -257,7 +257,7 @@
\end{matharray}
\begin{rail}
- 'declaration' target? text
+ 'declaration' ('(pervasive)')? target? text
;
'declare' target? (thmrefs + 'and')
;
@@ -271,6 +271,10 @@
function is transformed according to the morphisms being involved in
the interpretation hierarchy.
+ If the @{text "(pervasive)"} option is given, the corresponding
+ declaration is applied to all possible contexts involved, including
+ the global background theory.
+
\item @{command "declare"}~@{text thms} declares theorems to the
current local theory context. No theorem binding is involved here,
unlike @{command "theorems"} or @{command "lemmas"} (cf.\
--- a/doc-src/IsarRef/Thy/document/Misc.tex Sun Nov 08 15:45:09 2009 +0100
+++ b/doc-src/IsarRef/Thy/document/Misc.tex Sun Nov 08 20:50:31 2009 +0100
@@ -41,7 +41,7 @@
\end{matharray}
\begin{rail}
- 'print\_theory' ( '!'?)
+ ('print\_theory' | 'print\_theorems') ('!'?)
;
'find\_theorems' (('(' (nat)? ('with\_dups')? ')')?) (thmcriterion *)
@@ -76,8 +76,8 @@
\item \hyperlink{command.print-attributes}{\mbox{\isa{\isacommand{print{\isacharunderscore}attributes}}}} prints all attributes
available in the current theory context.
- \item \hyperlink{command.print-theorems}{\mbox{\isa{\isacommand{print{\isacharunderscore}theorems}}}} prints theorems resulting from
- the last command.
+ \item \hyperlink{command.print-theorems}{\mbox{\isa{\isacommand{print{\isacharunderscore}theorems}}}} prints theorems resulting from the
+ last command; the ``\isa{{\isachardoublequote}{\isacharbang}{\isachardoublequote}}'' option indicates extra verbosity.
\item \hyperlink{command.find-theorems}{\mbox{\isa{\isacommand{find{\isacharunderscore}theorems}}}}~\isa{criteria} retrieves facts
from the theory or proof context matching all of given search
--- a/doc-src/IsarRef/Thy/document/Spec.tex Sun Nov 08 15:45:09 2009 +0100
+++ b/doc-src/IsarRef/Thy/document/Spec.tex Sun Nov 08 20:50:31 2009 +0100
@@ -277,7 +277,7 @@
\end{matharray}
\begin{rail}
- 'declaration' target? text
+ 'declaration' ('(pervasive)')? target? text
;
'declare' target? (thmrefs + 'and')
;
@@ -291,6 +291,10 @@
function is transformed according to the morphisms being involved in
the interpretation hierarchy.
+ If the \isa{{\isachardoublequote}{\isacharparenleft}pervasive{\isacharparenright}{\isachardoublequote}} option is given, the corresponding
+ declaration is applied to all possible contexts involved, including
+ the global background theory.
+
\item \hyperlink{command.declare}{\mbox{\isa{\isacommand{declare}}}}~\isa{thms} declares theorems to the
current local theory context. No theorem binding is involved here,
unlike \hyperlink{command.theorems}{\mbox{\isa{\isacommand{theorems}}}} or \hyperlink{command.lemmas}{\mbox{\isa{\isacommand{lemmas}}}} (cf.\
--- a/src/HOL/Algebra/ringsimp.ML Sun Nov 08 15:45:09 2009 +0100
+++ b/src/HOL/Algebra/ringsimp.ML Sun Nov 08 20:50:31 2009 +0100
@@ -18,7 +18,7 @@
fun struct_eq ((s1: string, ts1), (s2, ts2)) =
(s1 = s2) andalso eq_list (op aconv) (ts1, ts2);
-structure Data = GenericDataFun
+structure Data = Generic_Data
(
type T = ((string * term list) * thm list) list;
(* Algebraic structures:
@@ -26,7 +26,7 @@
identifier and operations identify the structure uniquely. *)
val empty = [];
val extend = I;
- fun merge _ = AList.join struct_eq (K (Library.merge Thm.eq_thm_prop));
+ val merge = AList.join struct_eq (K Thm.merge_thms);
);
fun print_structures ctxt =
--- a/src/HOL/Boogie/Tools/boogie_split.ML Sun Nov 08 15:45:09 2009 +0100
+++ b/src/HOL/Boogie/Tools/boogie_split.ML Sun Nov 08 20:50:31 2009 +0100
@@ -18,13 +18,12 @@
(* sub-tactics store *)
-structure Sub_Tactics = TheoryDataFun
+structure Sub_Tactics = Theory_Data
(
type T = (Proof.context -> int -> tactic) Symtab.table
val empty = Symtab.empty
- val copy = I
val extend = I
- fun merge _ = Symtab.merge (K true)
+ fun merge data = Symtab.merge (K true) data
)
fun add_sub_tactic tac = Sub_Tactics.map (Symtab.update_new tac)
--- a/src/HOL/Boogie/Tools/boogie_vcs.ML Sun Nov 08 15:45:09 2009 +0100
+++ b/src/HOL/Boogie/Tools/boogie_vcs.ML Sun Nov 08 20:50:31 2009 +0100
@@ -19,14 +19,13 @@
fun err_vcs () = error "undischarged Boogie verification conditions found"
-structure VCs = TheoryDataFun
+structure VCs = Theory_Data
(
- type T = (Term.term * bool) Symtab.table option
+ type T = (term * bool) Symtab.table option
val empty = NONE
- val copy = I
val extend = I
- fun merge _ (NONE, NONE) = NONE
- | merge _ (_, _) = err_vcs ()
+ fun merge (NONE, NONE) = NONE
+ | merge _ = err_vcs ()
)
fun set vcs = VCs.map (fn
--- a/src/HOL/HOL.thy Sun Nov 08 15:45:09 2009 +0100
+++ b/src/HOL/HOL.thy Sun Nov 08 20:50:31 2009 +0100
@@ -1480,40 +1480,35 @@
ML {*
signature REORIENT_PROC =
sig
- val init : theory -> theory
val add : (term -> bool) -> theory -> theory
val proc : morphism -> simpset -> cterm -> thm option
end;
-structure ReorientProc : REORIENT_PROC =
+structure Reorient_Proc : REORIENT_PROC =
struct
- structure Data = TheoryDataFun
+ structure Data = Theory_Data
(
- type T = term -> bool;
- val empty = (fn _ => false);
- val copy = I;
+ type T = ((term -> bool) * stamp) list;
+ val empty = [];
val extend = I;
- fun merge _ (m1, m2) = (fn t => m1 t orelse m2 t);
- )
+ fun merge data : T = Library.merge (eq_snd op =) data;
+ );
+ fun add m = Data.map (cons (m, stamp ()));
+ fun matches thy t = exists (fn (m, _) => m t) (Data.get thy);
- val init = Data.init;
- fun add m = Data.map (fn matches => fn t => matches t orelse m t);
val meta_reorient = @{thm eq_commute [THEN eq_reflection]};
fun proc phi ss ct =
let
val ctxt = Simplifier.the_context ss;
val thy = ProofContext.theory_of ctxt;
- val matches = Data.get thy;
in
case Thm.term_of ct of
- (_ $ t $ u) => if matches u then NONE else SOME meta_reorient
+ (_ $ t $ u) => if matches thy u then NONE else SOME meta_reorient
| _ => NONE
end;
end;
*}
-setup ReorientProc.init
-
subsection {* Other simple lemmas and lemma duplicates *}
@@ -1560,14 +1555,14 @@
unfolding Let_def ..
setup {*
- ReorientProc.add
+ Reorient_Proc.add
(fn Const(@{const_name HOL.zero}, _) => true
| Const(@{const_name HOL.one}, _) => true
| _ => false)
*}
-simproc_setup reorient_zero ("0 = x") = ReorientProc.proc
-simproc_setup reorient_one ("1 = x") = ReorientProc.proc
+simproc_setup reorient_zero ("0 = x") = Reorient_Proc.proc
+simproc_setup reorient_one ("1 = x") = Reorient_Proc.proc
typed_print_translation {*
let
--- a/src/HOL/Import/hol4rews.ML Sun Nov 08 15:45:09 2009 +0100
+++ b/src/HOL/Import/hol4rews.ML Sun Nov 08 20:50:31 2009 +0100
@@ -11,25 +11,23 @@
| Generating of string
| Replaying of string
-structure HOL4DefThy = TheoryDataFun
+structure HOL4DefThy = Theory_Data
(
type T = ImportStatus
val empty = NoImport
- val copy = I
val extend = I
- fun merge _ (NoImport,NoImport) = NoImport
- | merge _ _ = (warning "Import status set during merge"; NoImport)
+ fun merge (NoImport, NoImport) = NoImport
+ | merge _ = (warning "Import status set during merge"; NoImport)
)
-structure ImportSegment = TheoryDataFun
+structure ImportSegment = Theory_Data
(
type T = string
val empty = ""
- val copy = I
val extend = I
- fun merge _ ("",arg) = arg
- | merge _ (arg,"") = arg
- | merge _ (s1,s2) =
+ fun merge ("",arg) = arg
+ | merge (arg,"") = arg
+ | merge (s1,s2) =
if s1 = s2
then s1
else error "Trying to merge two different import segments"
@@ -38,42 +36,38 @@
val get_import_segment = ImportSegment.get
val set_import_segment = ImportSegment.put
-structure HOL4UNames = TheoryDataFun
+structure HOL4UNames = Theory_Data
(
type T = string list
val empty = []
- val copy = I
val extend = I
- fun merge _ ([],[]) = []
- | merge _ _ = error "Used names not empty during merge"
+ fun merge ([], []) = []
+ | merge _ = error "Used names not empty during merge"
)
-structure HOL4Dump = TheoryDataFun
+structure HOL4Dump = Theory_Data
(
type T = string * string * string list
val empty = ("","",[])
- val copy = I
val extend = I
- fun merge _ (("","",[]),("","",[])) = ("","",[])
- | merge _ _ = error "Dump data not empty during merge"
+ fun merge (("","",[]),("","",[])) = ("","",[])
+ | merge _ = error "Dump data not empty during merge"
)
-structure HOL4Moves = TheoryDataFun
+structure HOL4Moves = Theory_Data
(
type T = string Symtab.table
val empty = Symtab.empty
- val copy = I
val extend = I
- fun merge _ : T * T -> T = Symtab.merge (K true)
+ fun merge data = Symtab.merge (K true) data
)
-structure HOL4Imports = TheoryDataFun
+structure HOL4Imports = Theory_Data
(
type T = string Symtab.table
val empty = Symtab.empty
- val copy = I
val extend = I
- fun merge _ : T * T -> T = Symtab.merge (K true)
+ fun merge data = Symtab.merge (K true) data
)
fun get_segment2 thyname thy =
@@ -87,85 +81,76 @@
HOL4Imports.put imps' thy
end
-structure HOL4CMoves = TheoryDataFun
+structure HOL4CMoves = Theory_Data
(
type T = string Symtab.table
val empty = Symtab.empty
- val copy = I
val extend = I
- fun merge _ : T * T -> T = Symtab.merge (K true)
+ fun merge data = Symtab.merge (K true) data
)
-structure HOL4Maps = TheoryDataFun
+structure HOL4Maps = Theory_Data
(
- type T = (string option) StringPair.table
+ type T = string option StringPair.table
val empty = StringPair.empty
- val copy = I
val extend = I
- fun merge _ : T * T -> T = StringPair.merge (K true)
+ fun merge data = StringPair.merge (K true) data
)
-structure HOL4Thms = TheoryDataFun
+structure HOL4Thms = Theory_Data
(
type T = holthm StringPair.table
val empty = StringPair.empty
- val copy = I
val extend = I
- fun merge _ : T * T -> T = StringPair.merge (K true)
+ fun merge data = StringPair.merge (K true) data
)
-structure HOL4ConstMaps = TheoryDataFun
+structure HOL4ConstMaps = Theory_Data
(
type T = (bool * string * typ option) StringPair.table
val empty = StringPair.empty
- val copy = I
val extend = I
- fun merge _ : T * T -> T = StringPair.merge (K true)
+ fun merge data = StringPair.merge (K true) data
)
-structure HOL4Rename = TheoryDataFun
+structure HOL4Rename = Theory_Data
(
type T = string StringPair.table
val empty = StringPair.empty
- val copy = I
val extend = I
- fun merge _ : T * T -> T = StringPair.merge (K true)
+ fun merge data = StringPair.merge (K true) data
)
-structure HOL4DefMaps = TheoryDataFun
+structure HOL4DefMaps = Theory_Data
(
type T = string StringPair.table
val empty = StringPair.empty
- val copy = I
val extend = I
- fun merge _ : T * T -> T = StringPair.merge (K true)
+ fun merge data = StringPair.merge (K true) data
)
-structure HOL4TypeMaps = TheoryDataFun
+structure HOL4TypeMaps = Theory_Data
(
type T = (bool * string) StringPair.table
val empty = StringPair.empty
- val copy = I
val extend = I
- fun merge _ : T * T -> T = StringPair.merge (K true)
+ fun merge data = StringPair.merge (K true) data
)
-structure HOL4Pending = TheoryDataFun
+structure HOL4Pending = Theory_Data
(
type T = ((term * term) list * thm) StringPair.table
val empty = StringPair.empty
- val copy = I
val extend = I
- fun merge _ : T * T -> T = StringPair.merge (K true)
+ fun merge data = StringPair.merge (K true) data
)
-structure HOL4Rewrites = TheoryDataFun
+structure HOL4Rewrites = Theory_Data
(
type T = thm list
val empty = []
- val copy = I
val extend = I
- fun merge _ = Library.merge Thm.eq_thm_prop
+ val merge = Thm.merge_thms
)
val hol4_debug = Unsynchronized.ref false
--- a/src/HOL/Import/import.ML Sun Nov 08 15:45:09 2009 +0100
+++ b/src/HOL/Import/import.ML Sun Nov 08 20:50:31 2009 +0100
@@ -9,13 +9,12 @@
val setup : theory -> theory
end
-structure ImportData = TheoryDataFun
+structure ImportData = Theory_Data
(
- type T = ProofKernel.thm option array option
+ type T = ProofKernel.thm option array option (* FIXME mutable array !??!!! *)
val empty = NONE
- val copy = I
val extend = I
- fun merge _ _ = NONE
+ fun merge _ = NONE
)
structure Import :> IMPORT =
--- a/src/HOL/Import/shuffler.ML Sun Nov 08 15:45:09 2009 +0100
+++ b/src/HOL/Import/shuffler.ML Sun Nov 08 20:50:31 2009 +0100
@@ -72,13 +72,12 @@
| _ => raise THM("Not an equality",0,[th]))
handle _ => raise THM("Couldn't make object equality",0,[th]) (* FIXME avoid handle _ *)
-structure ShuffleData = TheoryDataFun
+structure ShuffleData = Theory_Data
(
type T = thm list
val empty = []
- val copy = I
val extend = I
- fun merge _ = Library.merge Thm.eq_thm_prop
+ val merge = Thm.merge_thms
)
fun print_shuffles thy =
--- a/src/HOL/Int.thy Sun Nov 08 15:45:09 2009 +0100
+++ b/src/HOL/Int.thy Sun Nov 08 20:50:31 2009 +0100
@@ -1502,11 +1502,11 @@
declaration {* K Int_Arith.setup *}
setup {*
- ReorientProc.add
+ Reorient_Proc.add
(fn Const (@{const_name number_of}, _) $ _ => true | _ => false)
*}
-simproc_setup reorient_numeral ("number_of w = x") = ReorientProc.proc
+simproc_setup reorient_numeral ("number_of w = x") = Reorient_Proc.proc
subsection{*Lemmas About Small Numerals*}
--- a/src/HOL/Library/reify_data.ML Sun Nov 08 15:45:09 2009 +0100
+++ b/src/HOL/Library/reify_data.ML Sun Nov 08 20:50:31 2009 +0100
@@ -17,12 +17,13 @@
structure Reify_Data : REIFY_DATA =
struct
-structure Data = GenericDataFun
+structure Data = Generic_Data
(
type T = thm list * thm list;
val empty = ([], []);
val extend = I;
- fun merge _ = pairself Thm.merge_thms;
+ fun merge ((ths1, rths1), (ths2, rths2)) =
+ (Thm.merge_thms (ths1, ths2), Thm.merge_thms (rths1, rths2));
);
val get = Data.get o Context.Proof;
--- a/src/HOL/Mirabelle/Tools/mirabelle.ML Sun Nov 08 15:45:09 2009 +0100
+++ b/src/HOL/Mirabelle/Tools/mirabelle.ML Sun Nov 08 20:50:31 2009 +0100
@@ -60,13 +60,12 @@
type run_action = int -> run_args -> unit
type action = init_action * run_action * done_action
-structure Actions = TheoryDataFun
+structure Actions = Theory_Data
(
type T = (int * run_action * done_action) list
val empty = []
- val copy = I
val extend = I
- fun merge _ = Library.merge (K true)
+ fun merge data = Library.merge (K true) data (* FIXME ?!? *)
)
--- a/src/HOL/NSA/transfer.ML Sun Nov 08 15:45:09 2009 +0100
+++ b/src/HOL/NSA/transfer.ML Sun Nov 08 20:50:31 2009 +0100
@@ -15,7 +15,7 @@
structure Transfer: TRANSFER =
struct
-structure TransferData = GenericDataFun
+structure TransferData = Generic_Data
(
type T = {
intros: thm list,
@@ -25,15 +25,15 @@
};
val empty = {intros = [], unfolds = [], refolds = [], consts = []};
val extend = I;
- fun merge _
+ fun merge
({intros = intros1, unfolds = unfolds1,
refolds = refolds1, consts = consts1},
{intros = intros2, unfolds = unfolds2,
- refolds = refolds2, consts = consts2}) =
+ refolds = refolds2, consts = consts2}) : T =
{intros = Thm.merge_thms (intros1, intros2),
unfolds = Thm.merge_thms (unfolds1, unfolds2),
refolds = Thm.merge_thms (refolds1, refolds2),
- consts = Library.merge (op =) (consts1, consts2)} : T;
+ consts = Library.merge (op =) (consts1, consts2)};
);
fun unstar_typ (Type ("StarDef.star",[t])) = unstar_typ t
--- a/src/HOL/Nominal/nominal_atoms.ML Sun Nov 08 15:45:09 2009 +0100
+++ b/src/HOL/Nominal/nominal_atoms.ML Sun Nov 08 20:50:31 2009 +0100
@@ -42,13 +42,12 @@
cp_inst : thm Symtab.table,
dj_thms : thm Symtab.table};
-structure NominalData = TheoryDataFun
+structure NominalData = Theory_Data
(
type T = atom_info Symtab.table;
val empty = Symtab.empty;
- val copy = I;
val extend = I;
- fun merge _ x = Symtab.merge (K true) x;
+ fun merge data = Symtab.merge (K true) data;
);
fun make_atom_info ((((((pt_class, fs_class), cp_classes), at_inst), pt_inst), cp_inst), dj_thms) =
--- a/src/HOL/Nominal/nominal_datatype.ML Sun Nov 08 15:45:09 2009 +0100
+++ b/src/HOL/Nominal/nominal_datatype.ML Sun Nov 08 20:50:31 2009 +0100
@@ -84,13 +84,12 @@
distinct : thm list,
inject : thm list};
-structure NominalDatatypesData = TheoryDataFun
+structure NominalDatatypesData = Theory_Data
(
type T = nominal_datatype_info Symtab.table;
val empty = Symtab.empty;
- val copy = I;
val extend = I;
- fun merge _ tabs : T = Symtab.merge (K true) tabs;
+ fun merge data = Symtab.merge (K true) data;
);
val get_nominal_datatypes = NominalDatatypesData.get;
--- a/src/HOL/Nominal/nominal_thmdecls.ML Sun Nov 08 15:45:09 2009 +0100
+++ b/src/HOL/Nominal/nominal_thmdecls.ML Sun Nov 08 20:50:31 2009 +0100
@@ -25,12 +25,12 @@
structure NominalThmDecls: NOMINAL_THMDECLS =
struct
-structure Data = GenericDataFun
+structure Data = Generic_Data
(
type T = thm list
- val empty = []:T
+ val empty = []
val extend = I
- fun merge _ (r1:T, r2:T) = Thm.merge_thms (r1, r2)
+ val merge = Thm.merge_thms
)
(* Exception for when a theorem does not conform with form of an equivariance lemma. *)
--- a/src/HOL/Orderings.thy Sun Nov 08 15:45:09 2009 +0100
+++ b/src/HOL/Orderings.thy Sun Nov 08 20:50:31 2009 +0100
@@ -302,7 +302,7 @@
fun struct_eq ((s1: string, ts1), (s2, ts2)) =
(s1 = s2) andalso eq_list (op aconv) (ts1, ts2);
-structure Data = GenericDataFun
+structure Data = Generic_Data
(
type T = ((string * term list) * Order_Tac.less_arith) list;
(* Order structures:
@@ -311,7 +311,7 @@
identifier and operations identify the structure uniquely. *)
val empty = [];
val extend = I;
- fun merge _ = AList.join struct_eq (K fst);
+ fun merge data = AList.join struct_eq (K fst) data;
);
fun print_structures ctxt =
--- a/src/HOL/SMT/Tools/smt_solver.ML Sun Nov 08 15:45:09 2009 +0100
+++ b/src/HOL/SMT/Tools/smt_solver.ML Sun Nov 08 20:50:31 2009 +0100
@@ -204,13 +204,12 @@
type solver = Proof.context -> thm list -> thm
type solver_info = Context.generic -> Pretty.T list
-structure Solvers = TheoryDataFun
+structure Solvers = Theory_Data
(
type T = ((Proof.context -> solver_config) * solver_info) Symtab.table
val empty = Symtab.empty
- val copy = I
val extend = I
- fun merge _ = Symtab.merge (K true)
+ fun merge data = Symtab.merge (K true) data
handle Symtab.DUP name => error ("Duplicate SMT solver: " ^ quote name)
)
@@ -223,12 +222,13 @@
(* selected solver *)
-structure SelectedSolver = GenericDataFun
+structure SelectedSolver = Generic_Data
(
type T = serial * string
val empty = (serial (), no_solver)
val extend = I
- fun merge _ (sl1 as (s1, _), sl2 as (s2, _)) = if s1 > s2 then sl1 else sl2
+ fun merge (sl1 as (s1, _), sl2 as (s2, _)) =
+ if s1 > s2 then sl1 else sl2 (* FIXME depends on accidental load order !?! *)
)
val solver_name_of = snd o SelectedSolver.get
--- a/src/HOL/SMT/Tools/z3_proof_rules.ML Sun Nov 08 15:45:09 2009 +0100
+++ b/src/HOL/SMT/Tools/z3_proof_rules.ML Sun Nov 08 20:50:31 2009 +0100
@@ -1091,12 +1091,12 @@
val name = "z3_rewrite"
val descr = "Z3 rewrite rules used in proof reconstruction"
- structure Data = GenericDataFun
+ structure Data = Generic_Data
(
type T = thm Net.net
val empty = Net.empty
val extend = I
- fun merge _ = Net.merge Thm.eq_thm_prop
+ val merge = Net.merge Thm.eq_thm_prop
)
val get = Data.get o Context.Proof
--- a/src/HOL/Statespace/state_fun.ML Sun Nov 08 15:45:09 2009 +0100
+++ b/src/HOL/Statespace/state_fun.ML Sun Nov 08 20:50:31 2009 +0100
@@ -93,20 +93,16 @@
val ex_lookup_ss = HOL_ss addsimps @{thms StateFun.ex_id};
-structure StateFunArgs =
-struct
- type T = (simpset * simpset * bool);
+
+structure StateFunData = Generic_Data
+(
+ type T = simpset * simpset * bool;
(* lookup simpset, ex_lookup simpset, are simprocs installed *)
val empty = (empty_ss, empty_ss, false);
val extend = I;
- fun merge pp ((ss1,ex_ss1,b1),(ss2,ex_ss2,b2)) =
- (merge_ss (ss1,ss2)
- ,merge_ss (ex_ss1,ex_ss2)
- ,b1 orelse b2);
-end;
-
-
-structure StateFunData = GenericDataFun(StateFunArgs);
+ fun merge ((ss1, ex_ss1, b1), (ss2, ex_ss2, b2)) =
+ (merge_ss (ss1, ss2), merge_ss (ex_ss1, ex_ss2), b1 orelse b2);
+);
val init_state_fun_data =
Context.theory_map (StateFunData.put (lookup_ss,ex_lookup_ss,false));
--- a/src/HOL/Statespace/state_space.ML Sun Nov 08 15:45:09 2009 +0100
+++ b/src/HOL/Statespace/state_space.ML Sun Nov 08 20:50:31 2009 +0100
@@ -106,19 +106,18 @@
silent: bool
};
-structure NameSpaceArgs =
-struct
+structure NameSpaceData = Generic_Data
+(
type T = namespace_info;
val empty = {declinfo = Termtab.empty, distinctthm = Symtab.empty, silent = false};
val extend = I;
- fun merge pp ({declinfo=declinfo1, distinctthm=distinctthm1, silent=silent1},
- {declinfo=declinfo2, distinctthm=distinctthm2, silent=silent2}) =
- {declinfo = Termtab.merge (K true) (declinfo1, declinfo2),
- distinctthm = Symtab.merge (K true) (distinctthm1, distinctthm2),
- silent = silent1 andalso silent2}
-end;
-
-structure NameSpaceData = GenericDataFun(NameSpaceArgs);
+ fun merge
+ ({declinfo=declinfo1, distinctthm=distinctthm1, silent=silent1},
+ {declinfo=declinfo2, distinctthm=distinctthm2, silent=silent2}) : T =
+ {declinfo = Termtab.merge (K true) (declinfo1, declinfo2),
+ distinctthm = Symtab.merge (K true) (distinctthm1, distinctthm2),
+ silent = silent1 andalso silent2}
+);
fun make_namespace_data declinfo distinctthm silent =
{declinfo=declinfo,distinctthm=distinctthm,silent=silent};
@@ -172,17 +171,13 @@
types: typ list (* range types of state space *)
};
-structure StateSpaceArgs =
-struct
- val name = "HOL/StateSpace";
+structure StateSpaceData = Generic_Data
+(
type T = statespace_info Symtab.table;
val empty = Symtab.empty;
val extend = I;
-
- fun merge pp (nt1,nt2) = Symtab.merge (K true) (nt1, nt2);
-end;
-
-structure StateSpaceData = GenericDataFun(StateSpaceArgs);
+ fun merge data : T = Symtab.merge (K true) data;
+);
fun add_statespace name args parents components types ctxt =
StateSpaceData.put
--- a/src/HOL/Tools/ATP_Manager/atp_manager.ML Sun Nov 08 15:45:09 2009 +0100
+++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML Sun Nov 08 20:50:31 2009 +0100
@@ -226,13 +226,12 @@
fun err_dup_prover name = error ("Duplicate prover: " ^ quote name);
-structure Provers = TheoryDataFun
+structure Provers = Theory_Data
(
type T = (ATP_Wrapper.prover * stamp) Symtab.table;
val empty = Symtab.empty;
- val copy = I;
val extend = I;
- fun merge _ tabs : T = Symtab.merge (eq_snd op =) tabs
+ fun merge data : T = Symtab.merge (eq_snd op =) data
handle Symtab.DUP dup => err_dup_prover dup;
);
--- a/src/HOL/Tools/Datatype/datatype.ML Sun Nov 08 15:45:09 2009 +0100
+++ b/src/HOL/Tools/Datatype/datatype.ML Sun Nov 08 20:50:31 2009 +0100
@@ -42,7 +42,7 @@
(* data management *)
-structure DatatypesData = TheoryDataFun
+structure DatatypesData = Theory_Data
(
type T =
{types: info Symtab.table,
@@ -51,11 +51,10 @@
val empty =
{types = Symtab.empty, constrs = Symtab.empty, cases = Symtab.empty};
- val copy = I;
val extend = I;
- fun merge _
+ fun merge
({types = types1, constrs = constrs1, cases = cases1},
- {types = types2, constrs = constrs2, cases = cases2}) =
+ {types = types2, constrs = constrs2, cases = cases2}) : T =
{types = Symtab.merge (K true) (types1, types2),
constrs = Symtab.join (K (AList.merge (op =) (K true))) (constrs1, constrs2),
cases = Symtab.merge (K true) (cases1, cases2)};
--- a/src/HOL/Tools/Function/context_tree.ML Sun Nov 08 15:45:09 2009 +0100
+++ b/src/HOL/Tools/Function/context_tree.ML Sun Nov 08 20:50:31 2009 +0100
@@ -44,12 +44,12 @@
open Function_Common
open Function_Lib
-structure FunctionCongs = GenericDataFun
+structure FunctionCongs = Generic_Data
(
type T = thm list
val empty = []
val extend = I
- fun merge _ = Thm.merge_thms
+ val merge = Thm.merge_thms
);
val get_function_congs = FunctionCongs.get o Context.Proof
--- a/src/HOL/Tools/Function/function_common.ML Sun Nov 08 15:45:09 2009 +0100
+++ b/src/HOL/Tools/Function/function_common.ML Sun Nov 08 20:50:31 2009 +0100
@@ -27,12 +27,12 @@
(* Termination rules *)
-structure TerminationRule = GenericDataFun
+structure TerminationRule = Generic_Data
(
type T = thm list
val empty = []
val extend = I
- fun merge _ = Thm.merge_thms
+ val merge = Thm.merge_thms
);
val get_termination_rules = TerminationRule.get
@@ -90,13 +90,12 @@
defname = name defname }
end
-structure FunctionData = GenericDataFun
+structure FunctionData = Generic_Data
(
type T = (term * function_context_data) Item_Net.T;
val empty : T = Item_Net.init (op aconv o pairself fst) (single o fst);
- val copy = I;
val extend = I;
- fun merge _ (tab1, tab2) = Item_Net.merge (tab1, tab2)
+ fun merge tabs : T = Item_Net.merge tabs;
);
val get_function = FunctionData.get o Context.Proof;
@@ -152,12 +151,12 @@
(* Default Termination Prover *)
-structure TerminationProver = GenericDataFun
+structure TerminationProver = Generic_Data
(
type T = Proof.context -> Proof.method
val empty = (fn _ => error "Termination prover not configured")
val extend = I
- fun merge _ (a,b) = b (* FIXME *)
+ fun merge (a, b) = b (* FIXME ? *)
);
val set_termination_prover = TerminationProver.put
@@ -310,12 +309,12 @@
(ts, curry op ~~ bnds o Library.unflat tss, sort, cnames)
end
-structure Preprocessor = GenericDataFun
+structure Preprocessor = Generic_Data
(
type T = preproc
val empty : T = empty_preproc check_defs
val extend = I
- fun merge _ (a, _) = a
+ fun merge (a, _) = a
);
val get_preproc = Preprocessor.get o Context.Proof
--- a/src/HOL/Tools/Function/scnp_reconstruct.ML Sun Nov 08 15:45:09 2009 +0100
+++ b/src/HOL/Tools/Function/scnp_reconstruct.ML Sun Nov 08 20:50:31 2009 +0100
@@ -63,13 +63,12 @@
reduction_pair : thm
}
-structure Multiset_Setup = TheoryDataFun
+structure Multiset_Setup = Theory_Data
(
type T = multiset_setup option
val empty = NONE
- val copy = I;
val extend = I;
- fun merge _ (v1, v2) = if is_some v2 then v2 else v1
+ fun merge (v1, v2) = if is_some v2 then v2 else v1 (* FIXME prefer v1 !?! *)
)
val multiset_setup = Multiset_Setup.put o SOME
--- a/src/HOL/Tools/Function/size.ML Sun Nov 08 15:45:09 2009 +0100
+++ b/src/HOL/Tools/Function/size.ML Sun Nov 08 20:50:31 2009 +0100
@@ -15,13 +15,12 @@
open DatatypeAux;
-structure SizeData = TheoryDataFun
+structure SizeData = Theory_Data
(
type T = (string * thm list) Symtab.table;
val empty = Symtab.empty;
- val copy = I
val extend = I
- fun merge _ = Symtab.merge (K true);
+ fun merge data = Symtab.merge (K true) data;
);
val lookup_size = SizeData.get #> Symtab.lookup;
--- a/src/HOL/Tools/Groebner_Basis/normalizer_data.ML Sun Nov 08 15:45:09 2009 +0100
+++ b/src/HOL/Tools/Groebner_Basis/normalizer_data.ML Sun Nov 08 20:50:31 2009 +0100
@@ -40,12 +40,12 @@
val eq_key = Thm.eq_thm;
fun eq_data arg = eq_fst eq_key arg;
-structure Data = GenericDataFun
+structure Data = Generic_Data
(
type T = simpset * (thm * entry) list;
val empty = (HOL_basic_ss, []);
val extend = I;
- fun merge _ ((ss, e), (ss', e')) =
+ fun merge ((ss, e), (ss', e')) : T =
(merge_ss (ss, ss'), AList.merge eq_key (K true) (e, e'));
);
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Sun Nov 08 15:45:09 2009 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Sun Nov 08 20:50:31 2009 +0100
@@ -179,14 +179,13 @@
unrolled_preds: unrolled list Unsynchronized.ref,
wf_cache: wf_cache Unsynchronized.ref}
-structure TheoryData = TheoryDataFun(
+structure TheoryData = Theory_Data(
type T = {frac_types: (string * (string * string) list) list,
codatatypes: (string * (string * styp list)) list}
val empty = {frac_types = [], codatatypes = []}
- val copy = I
val extend = I
- fun merge _ ({frac_types = fs1, codatatypes = cs1},
- {frac_types = fs2, codatatypes = cs2}) =
+ fun merge ({frac_types = fs1, codatatypes = cs1},
+ {frac_types = fs2, codatatypes = cs2}) : T =
{frac_types = AList.merge (op =) (op =) (fs1, fs2),
codatatypes = AList.merge (op =) (op =) (cs1, cs2)})
--- a/src/HOL/Tools/Nitpick/nitpick_isar.ML Sun Nov 08 15:45:09 2009 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_isar.ML Sun Nov 08 20:50:31 2009 +0100
@@ -125,13 +125,12 @@
| _ => value)
| NONE => (name, value)
-structure TheoryData = TheoryDataFun(
+structure TheoryData = Theory_Data(
type T = {params: raw_param list, registered_auto: bool}
val empty = {params = rev default_default_params, registered_auto = false}
- val copy = I
val extend = I
- fun merge _ ({params = ps1, registered_auto = a1},
- {params = ps2, registered_auto = a2}) =
+ fun merge ({params = ps1, registered_auto = a1},
+ {params = ps2, registered_auto = a2}) : T =
{params = AList.merge (op =) (op =) (ps1, ps2),
registered_auto = a1 orelse a2})
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Sun Nov 08 15:45:09 2009 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Sun Nov 08 20:50:31 2009 +0100
@@ -232,13 +232,12 @@
eq_option (Thm.eq_thm) (#elim d1, #elim d2) andalso
#nparams d1 = #nparams d2
-structure PredData = TheoryDataFun
+structure PredData = Theory_Data
(
type T = pred_data Graph.T;
val empty = Graph.empty;
- val copy = I;
val extend = I;
- fun merge _ = Graph.merge eq_pred_data;
+ val merge = Graph.merge eq_pred_data;
);
(* queries *)
@@ -2450,7 +2449,7 @@
(*FIXME name discrepancy in attribs and ML code*)
(*FIXME intros should be better named intro*)
-(* TODO: make TheoryDataFun to GenericDataFun & remove duplication of local theory and theory *)
+(* TODO: make Theory_Data to Generic_Data & remove duplication of local theory and theory *)
fun generic_code_pred prep_const options raw_const lthy =
let
val thy = ProofContext.theory_of lthy
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML Sun Nov 08 15:45:09 2009 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML Sun Nov 08 20:50:31 2009 +0100
@@ -19,15 +19,14 @@
open Predicate_Compile_Aux;
-structure Data = TheoryDataFun
+structure Data = Theory_Data
(
type T =
{const_spec_table : thm list Symtab.table};
val empty =
{const_spec_table = Symtab.empty};
- val copy = I;
val extend = I;
- fun merge _
+ fun merge
({const_spec_table = const_spec_table1},
{const_spec_table = const_spec_table2}) =
{const_spec_table = Symtab.merge (K true) (const_spec_table1, const_spec_table2)}
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML Sun Nov 08 15:45:09 2009 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML Sun Nov 08 20:50:31 2009 +0100
@@ -56,13 +56,12 @@
fun is_constr thy = is_some o Code.get_datatype_of_constr thy;
(* Table from constant name (string) to term of inductive predicate *)
-structure Pred_Compile_Preproc = TheoryDataFun
+structure Pred_Compile_Preproc = Theory_Data
(
type T = string Symtab.table;
val empty = Symtab.empty;
- val copy = I;
val extend = I;
- fun merge _ = Symtab.merge (op =);
+ fun merge data : T = Symtab.merge (op =) data; (* FIXME handle Symtab.DUP ?? *)
)
fun pred_of_function thy name = Symtab.lookup (Pred_Compile_Preproc.get thy) name
--- a/src/HOL/Tools/Qelim/cooper_data.ML Sun Nov 08 15:45:09 2009 +0100
+++ b/src/HOL/Tools/Qelim/cooper_data.ML Sun Nov 08 20:50:31 2009 +0100
@@ -44,12 +44,12 @@
@{term "0::int"}, @{term "1::int"}, @{term "0::nat"}, @{term "1::nat"},
@{term "True"}, @{term "False"}];
-structure Data = GenericDataFun
+structure Data = Generic_Data
(
- type T = simpset * (term list);
+ type T = simpset * term list;
val empty = (start_ss, allowed_consts);
val extend = I;
- fun merge _ ((ss1, ts1), (ss2, ts2)) =
+ fun merge ((ss1, ts1), (ss2, ts2)) =
(merge_ss (ss1, ss2), Library.merge (op aconv) (ts1, ts2));
);
--- a/src/HOL/Tools/Qelim/ferrante_rackoff_data.ML Sun Nov 08 15:45:09 2009 +0100
+++ b/src/HOL/Tools/Qelim/ferrante_rackoff_data.ML Sun Nov 08 20:50:31 2009 +0100
@@ -38,12 +38,12 @@
val eq_key = Thm.eq_thm;
fun eq_data arg = eq_fst eq_key arg;
-structure Data = GenericDataFun
+structure Data = Generic_Data
(
type T = (thm * entry) list;
val empty = [];
val extend = I;
- fun merge _ = AList.merge eq_key (K true);
+ fun merge data : T = AList.merge eq_key (K true) data;
);
val get = Data.get o Context.Proof;
--- a/src/HOL/Tools/Qelim/langford_data.ML Sun Nov 08 15:45:09 2009 +0100
+++ b/src/HOL/Tools/Qelim/langford_data.ML Sun Nov 08 20:50:31 2009 +0100
@@ -17,12 +17,13 @@
val eq_key = Thm.eq_thm;
fun eq_data arg = eq_fst eq_key arg;
-structure Data = GenericDataFun
-( type T = simpset * (thm * entry) list;
+structure Data = Generic_Data
+(
+ type T = simpset * (thm * entry) list;
val empty = (HOL_basic_ss, []);
val extend = I;
- fun merge _ ((ss1,es1), (ss2,es2)) =
- (merge_ss (ss1,ss2), AList.merge eq_key (K true) (es1,es2));;
+ fun merge ((ss1, es1), (ss2, es2)) : T =
+ (merge_ss (ss1, ss2), AList.merge eq_key (K true) (es1, es2));
);
val get = Data.get o Context.Proof;
--- a/src/HOL/Tools/arith_data.ML Sun Nov 08 15:45:09 2009 +0100
+++ b/src/HOL/Tools/arith_data.ML Sun Nov 08 20:50:31 2009 +0100
@@ -41,13 +41,12 @@
val get_arith_facts = Arith_Facts.get;
-structure Arith_Tactics = TheoryDataFun
+structure Arith_Tactics = Theory_Data
(
type T = (serial * (string * (bool -> Proof.context -> int -> tactic))) list;
val empty = [];
- val copy = I;
val extend = I;
- fun merge _ = AList.merge (op =) (K true);
+ fun merge data : T = AList.merge (op =) (K true) data;
);
fun add_tactic name tac = Arith_Tactics.map (cons (serial (), (name, tac)));
--- a/src/HOL/Tools/inductive.ML Sun Nov 08 15:45:09 2009 +0100
+++ b/src/HOL/Tools/inductive.ML Sun Nov 08 20:50:31 2009 +0100
@@ -136,12 +136,12 @@
type inductive_info =
{names: string list, coind: bool} * inductive_result;
-structure InductiveData = GenericDataFun
+structure InductiveData = Generic_Data
(
type T = inductive_info Symtab.table * thm list;
val empty = (Symtab.empty, []);
val extend = I;
- fun merge _ ((tab1, monos1), (tab2, monos2)) =
+ fun merge ((tab1, monos1), (tab2, monos2)) : T =
(Symtab.merge (K true) (tab1, tab2), Thm.merge_thms (monos1, monos2));
);
--- a/src/HOL/Tools/inductive_codegen.ML Sun Nov 08 15:45:09 2009 +0100
+++ b/src/HOL/Tools/inductive_codegen.ML Sun Nov 08 20:50:31 2009 +0100
@@ -20,7 +20,7 @@
fun merge_rules tabs =
Symtab.join (fn _ => AList.merge (Thm.eq_thm_prop) (K true)) tabs;
-structure CodegenData = TheoryDataFun
+structure CodegenData = Theory_Data
(
type T =
{intros : (thm * (string * int)) list Symtab.table,
@@ -28,10 +28,9 @@
eqns : (thm * string) list Symtab.table};
val empty =
{intros = Symtab.empty, graph = Graph.empty, eqns = Symtab.empty};
- val copy = I;
val extend = I;
- fun merge _ ({intros=intros1, graph=graph1, eqns=eqns1},
- {intros=intros2, graph=graph2, eqns=eqns2}) =
+ fun merge ({intros=intros1, graph=graph1, eqns=eqns1},
+ {intros=intros2, graph=graph2, eqns=eqns2}) : T =
{intros = merge_rules (intros1, intros2),
graph = Graph.merge (K true) (graph1, graph2),
eqns = merge_rules (eqns1, eqns2)};
--- a/src/HOL/Tools/inductive_set.ML Sun Nov 08 15:45:09 2009 +0100
+++ b/src/HOL/Tools/inductive_set.ML Sun Nov 08 20:50:31 2009 +0100
@@ -152,7 +152,7 @@
(* where s and p are parameters *)
(***********************************************************)
-structure PredSetConvData = GenericDataFun
+structure PredSetConvData = Generic_Data
(
type T =
{(* rules for converting predicates to sets *)
@@ -166,7 +166,7 @@
val empty = {to_set_simps = [], to_pred_simps = [],
set_arities = Symtab.empty, pred_arities = Symtab.empty};
val extend = I;
- fun merge _
+ fun merge
({to_set_simps = to_set_simps1, to_pred_simps = to_pred_simps1,
set_arities = set_arities1, pred_arities = pred_arities1},
{to_set_simps = to_set_simps2, to_pred_simps = to_pred_simps2,
--- a/src/HOL/Tools/lin_arith.ML Sun Nov 08 15:45:09 2009 +0100
+++ b/src/HOL/Tools/lin_arith.ML Sun Nov 08 20:50:31 2009 +0100
@@ -72,17 +72,17 @@
(* arith context data *)
-structure Lin_Arith_Data = GenericDataFun
+structure Lin_Arith_Data = Generic_Data
(
type T = {splits: thm list,
inj_consts: (string * typ) list,
discrete: string list};
val empty = {splits = [], inj_consts = [], discrete = []};
val extend = I;
- fun merge _
+ fun merge
({splits= splits1, inj_consts= inj_consts1, discrete= discrete1},
{splits= splits2, inj_consts= inj_consts2, discrete= discrete2}) : T =
- {splits = Library.merge Thm.eq_thm_prop (splits1, splits2),
+ {splits = Thm.merge_thms (splits1, splits2),
inj_consts = Library.merge (op =) (inj_consts1, inj_consts2),
discrete = Library.merge (op =) (discrete1, discrete2)};
);
--- a/src/HOL/Tools/recdef.ML Sun Nov 08 15:45:09 2009 +0100
+++ b/src/HOL/Tools/recdef.ML Sun Nov 08 20:50:31 2009 +0100
@@ -86,18 +86,17 @@
type recdef_info = {simps: thm list, rules: thm list list, induct: thm, tcs: term list};
-structure GlobalRecdefData = TheoryDataFun
+structure GlobalRecdefData = Theory_Data
(
type T = recdef_info Symtab.table * hints;
val empty = (Symtab.empty, mk_hints ([], [], [])): T;
- val copy = I;
val extend = I;
- fun merge _
+ fun merge
((tab1, {simps = simps1, congs = congs1, wfs = wfs1}),
(tab2, {simps = simps2, congs = congs2, wfs = wfs2})) : T =
(Symtab.merge (K true) (tab1, tab2),
mk_hints (Thm.merge_thms (simps1, simps2),
- AList.merge (op =) Thm.eq_thm (congs1, congs2),
+ AList.merge (op =) Thm.eq_thm_prop (congs1, congs2),
Thm.merge_thms (wfs1, wfs2)));
);
@@ -115,7 +114,7 @@
(* proof data *)
-structure LocalRecdefData = ProofDataFun
+structure LocalRecdefData = Proof_Data
(
type T = hints;
val init = get_global_hints;
--- a/src/HOL/Tools/recfun_codegen.ML Sun Nov 08 15:45:09 2009 +0100
+++ b/src/HOL/Tools/recfun_codegen.ML Sun Nov 08 20:50:31 2009 +0100
@@ -16,13 +16,12 @@
val const_of = dest_Const o head_of o fst o Logic.dest_equals;
-structure ModuleData = TheoryDataFun
+structure ModuleData = Theory_Data
(
type T = string Symtab.table;
val empty = Symtab.empty;
- val copy = I;
val extend = I;
- fun merge _ = Symtab.merge (K true);
+ fun merge data = Symtab.merge (K true) data;
);
fun add_thm_target module_name thm thy =
--- a/src/HOL/Tools/record.ML Sun Nov 08 15:45:09 2009 +0100
+++ b/src/HOL/Tools/record.ML Sun Nov 08 20:50:31 2009 +0100
@@ -81,13 +81,12 @@
cterm_instantiate (map (apfst getvar) values) thm
end;
-structure IsTupleThms = TheoryDataFun
+structure IsTupleThms = Theory_Data
(
type T = thm Symtab.table;
val empty = Symtab.make [tuple_istuple];
- val copy = I;
val extend = I;
- fun merge _ = Symtab.merge Thm.eq_thm_prop;
+ fun merge data = Symtab.merge Thm.eq_thm_prop data; (* FIXME handle Symtab.DUP ?? *)
);
fun do_typedef name repT alphas thy =
@@ -381,7 +380,7 @@
equalities = equalities, extinjects=extinjects, extsplit = extsplit, splits = splits,
extfields = extfields, fieldext = fieldext }: record_data;
-structure RecordsData = TheoryDataFun
+structure RecordsData = Theory_Data
(
type T = record_data;
val empty =
@@ -390,10 +389,8 @@
simpset = HOL_basic_ss, defset = HOL_basic_ss,
foldcong = HOL_basic_ss, unfoldcong = HOL_basic_ss}
Symtab.empty [] Symtab.empty Symtab.empty Symtab.empty Symtab.empty;
-
- val copy = I;
val extend = I;
- fun merge _
+ fun merge
({records = recs1,
sel_upd =
{selectors = sels1, updates = upds1,
@@ -425,7 +422,7 @@
foldcong = Simplifier.merge_ss (fc1, fc2),
unfoldcong = Simplifier.merge_ss (uc1, uc2)}
(Symtab.merge Thm.eq_thm_prop (equalities1, equalities2))
- (Library.merge Thm.eq_thm_prop (extinjects1, extinjects2))
+ (Thm.merge_thms (extinjects1, extinjects2))
(Symtab.merge Thm.eq_thm_prop (extsplit1, extsplit2))
(Symtab.merge (fn ((a, b, c, d), (w, x, y, z)) =>
Thm.eq_thm (a, w) andalso Thm.eq_thm (b, x) andalso
--- a/src/HOL/Tools/refute.ML Sun Nov 08 15:45:09 2009 +0100
+++ b/src/HOL/Tools/refute.ML Sun Nov 08 20:50:31 2009 +0100
@@ -201,7 +201,7 @@
};
- structure RefuteData = TheoryDataFun
+ structure RefuteData = Theory_Data
(
type T =
{interpreters: (string * (theory -> model -> arguments -> term ->
@@ -210,11 +210,10 @@
(int -> bool) -> term option)) list,
parameters: string Symtab.table};
val empty = {interpreters = [], printers = [], parameters = Symtab.empty};
- val copy = I;
val extend = I;
- fun merge _
+ fun merge
({interpreters = in1, printers = pr1, parameters = pa1},
- {interpreters = in2, printers = pr2, parameters = pa2}) =
+ {interpreters = in2, printers = pr2, parameters = pa2}) : T =
{interpreters = AList.merge (op =) (K true) (in1, in2),
printers = AList.merge (op =) (K true) (pr1, pr2),
parameters = Symtab.merge (op=) (pa1, pa2)};
--- a/src/HOL/Tools/res_axioms.ML Sun Nov 08 15:45:09 2009 +0100
+++ b/src/HOL/Tools/res_axioms.ML Sun Nov 08 20:50:31 2009 +0100
@@ -349,13 +349,12 @@
(*The cache prevents repeated clausification of a theorem, and also repeated declaration of
Skolem functions.*)
-structure ThmCache = TheoryDataFun
+structure ThmCache = Theory_Data
(
type T = thm list Thmtab.table * unit Symtab.table;
val empty = (Thmtab.empty, Symtab.empty);
- val copy = I;
val extend = I;
- fun merge _ ((cache1, seen1), (cache2, seen2)) : T =
+ fun merge ((cache1, seen1), (cache2, seen2)) : T =
(Thmtab.merge (K true) (cache1, cache2), Symtab.merge (K true) (seen1, seen2));
);
--- a/src/HOL/Tools/res_blacklist.ML Sun Nov 08 15:45:09 2009 +0100
+++ b/src/HOL/Tools/res_blacklist.ML Sun Nov 08 20:50:31 2009 +0100
@@ -19,12 +19,12 @@
structure Res_Blacklist: RES_BLACKLIST =
struct
-structure Data = GenericDataFun
+structure Data = Generic_Data
(
type T = thm Termtab.table;
val empty = Termtab.empty;
val extend = I;
- fun merge _ tabs = Termtab.merge (K true) tabs;
+ fun merge tabs = Termtab.merge (K true) tabs;
);
fun blacklisted ctxt th =
--- a/src/HOL/Tools/transfer.ML Sun Nov 08 15:45:09 2009 +0100
+++ b/src/HOL/Tools/transfer.ML Sun Nov 08 20:50:31 2009 +0100
@@ -25,12 +25,12 @@
type data = simpset * (thm * entry) list;
-structure Data = GenericDataFun
+structure Data = Generic_Data
(
type T = data;
val empty = (HOL_ss, []);
val extend = I;
- fun merge _ ((ss1, e1), (ss2, e2)) =
+ fun merge ((ss1, e1), (ss2, e2)) : T =
(merge_ss (ss1, ss2), AList.join Thm.eq_thm (K merge_entry) (e1, e2));
);
--- a/src/HOL/Tools/typecopy.ML Sun Nov 08 15:45:09 2009 +0100
+++ b/src/HOL/Tools/typecopy.ML Sun Nov 08 20:50:31 2009 +0100
@@ -30,13 +30,12 @@
proj_def: thm
};
-structure TypecopyData = TheoryDataFun
+structure TypecopyData = Theory_Data
(
type T = info Symtab.table;
val empty = Symtab.empty;
- val copy = I;
val extend = I;
- fun merge _ = Symtab.merge (K true);
+ fun merge data = Symtab.merge (K true) data;
);
val get_info = Symtab.lookup o TypecopyData.get;
--- a/src/HOL/Tools/typedef.ML Sun Nov 08 15:45:09 2009 +0100
+++ b/src/HOL/Tools/typedef.ML Sun Nov 08 20:50:31 2009 +0100
@@ -36,13 +36,12 @@
Abs_inverse: thm, Rep_inject: thm, Abs_inject: thm, Rep_cases: thm, Abs_cases: thm,
Rep_induct: thm, Abs_induct: thm};
-structure TypedefData = TheoryDataFun
+structure TypedefData = Theory_Data
(
type T = info Symtab.table;
val empty = Symtab.empty;
- val copy = I;
val extend = I;
- fun merge _ tabs : T = Symtab.merge (K true) tabs;
+ fun merge data = Symtab.merge (K true) data;
);
val get_info = Symtab.lookup o TypedefData.get;
--- a/src/HOL/ex/Numeral.thy Sun Nov 08 15:45:09 2009 +0100
+++ b/src/HOL/ex/Numeral.thy Sun Nov 08 20:50:31 2009 +0100
@@ -923,22 +923,21 @@
declare Suc_of_num [simp]
-thm numeral
-
subsection {* Simplification Procedures *}
subsubsection {* Reorientation of equalities *}
setup {*
- ReorientProc.add
+ Reorient_Proc.add
(fn Const(@{const_name of_num}, _) $ _ => true
| Const(@{const_name uminus}, _) $
(Const(@{const_name of_num}, _) $ _) => true
| _ => false)
*}
-simproc_setup reorient_num ("of_num n = x" | "- of_num m = y") = ReorientProc.proc
+simproc_setup reorient_num ("of_num n = x" | "- of_num m = y") = Reorient_Proc.proc
+
subsubsection {* Constant folding for multiplication in semirings *}
--- a/src/HOLCF/Pcpo.thy Sun Nov 08 15:45:09 2009 +0100
+++ b/src/HOLCF/Pcpo.thy Sun Nov 08 20:50:31 2009 +0100
@@ -196,11 +196,11 @@
text {* Simproc to rewrite @{term "\<bottom> = x"} to @{term "x = \<bottom>"}. *}
setup {*
- ReorientProc.add
+ Reorient_Proc.add
(fn Const(@{const_name UU}, _) => true | _ => false)
*}
-simproc_setup reorient_bottom ("\<bottom> = x") = ReorientProc.proc
+simproc_setup reorient_bottom ("\<bottom> = x") = Reorient_Proc.proc
context pcpo
begin
--- a/src/HOLCF/Tools/fixrec.ML Sun Nov 08 15:45:09 2009 +0100
+++ b/src/HOLCF/Tools/fixrec.ML Sun Nov 08 20:50:31 2009 +0100
@@ -160,12 +160,12 @@
(************* fixed-point definitions and unfolding theorems ************)
(*************************************************************************)
-structure FixrecUnfoldData = GenericDataFun (
+structure FixrecUnfoldData = Generic_Data
+(
type T = thm Symtab.table;
val empty = Symtab.empty;
- val copy = I;
val extend = I;
- fun merge _ = Symtab.merge (K true);
+ fun merge data : T = Symtab.merge (K true) data;
);
local
@@ -252,12 +252,12 @@
(*********** monadic notation and pattern matching compilation ***********)
(*************************************************************************)
-structure FixrecMatchData = TheoryDataFun (
+structure FixrecMatchData = Theory_Data
+(
type T = string Symtab.table;
val empty = Symtab.empty;
- val copy = I;
val extend = I;
- fun merge _ = Symtab.merge (K true);
+ fun merge data = Symtab.merge (K true) data;
);
(* associate match functions with pattern constants *)
@@ -363,16 +363,16 @@
(********************** Proving associated theorems **********************)
(*************************************************************************)
-structure FixrecSimpData = GenericDataFun (
+structure FixrecSimpData = Generic_Data
+(
type T = simpset;
val empty =
HOL_basic_ss
addsimps simp_thms
addsimps [@{thm beta_cfun}]
addsimprocs [@{simproc cont_proc}];
- val copy = I;
val extend = I;
- fun merge _ = merge_ss;
+ val merge = merge_ss;
);
fun fixrec_simp_tac ctxt =
@@ -523,8 +523,7 @@
end;
val setup =
- FixrecMatchData.init
- #> Attrib.setup @{binding fixrec_simp}
+ Attrib.setup @{binding fixrec_simp}
(Attrib.add_del fixrec_simp_add fixrec_simp_del)
"declaration of fixrec simp rule"
#> Method.setup @{binding fixrec_simp}
--- a/src/Provers/Arith/fast_lin_arith.ML Sun Nov 08 15:45:09 2009 +0100
+++ b/src/Provers/Arith/fast_lin_arith.ML Sun Nov 08 20:50:31 2009 +0100
@@ -109,7 +109,7 @@
fun no_number_of _ _ _ = raise CTERM ("number_of", [])
-structure Data = GenericDataFun
+structure Data = Generic_Data
(
type T =
{add_mono_thms: thm list,
@@ -124,7 +124,7 @@
lessD = [], neqE = [], simpset = Simplifier.empty_ss,
number_of = (serial (), no_number_of) } : T;
val extend = I;
- fun merge _
+ fun merge
({add_mono_thms= add_mono_thms1, mult_mono_thms= mult_mono_thms1, inj_thms= inj_thms1,
lessD = lessD1, neqE=neqE1, simpset = simpset1,
number_of = (number_of1 as (s1, _))},
@@ -137,6 +137,7 @@
lessD = Thm.merge_thms (lessD1, lessD2),
neqE = Thm.merge_thms (neqE1, neqE2),
simpset = Simplifier.merge_ss (simpset1, simpset2),
+ (* FIXME depends on accidental load order !?! *)
number_of = if s1 > s2 then number_of1 else number_of2};
);
--- a/src/Provers/classical.ML Sun Nov 08 15:45:09 2009 +0100
+++ b/src/Provers/classical.ML Sun Nov 08 20:50:31 2009 +0100
@@ -835,13 +835,12 @@
(* global clasets *)
-structure GlobalClaset = TheoryDataFun
+structure GlobalClaset = Theory_Data
(
type T = claset * context_cs;
val empty = (empty_cs, empty_context_cs);
- val copy = I;
val extend = I;
- fun merge _ ((cs1, ctxt_cs1), (cs2, ctxt_cs2)) =
+ fun merge ((cs1, ctxt_cs1), (cs2, ctxt_cs2)) =
(merge_cs (cs1, cs2), merge_context_cs (ctxt_cs1, ctxt_cs2));
);
@@ -868,7 +867,7 @@
(* local clasets *)
-structure LocalClaset = ProofDataFun
+structure LocalClaset = Proof_Data
(
type T = claset;
val init = get_global_claset;
--- a/src/Pure/Isar/attrib.ML Sun Nov 08 15:45:09 2009 +0100
+++ b/src/Pure/Isar/attrib.ML Sun Nov 08 20:50:31 2009 +0100
@@ -65,13 +65,12 @@
(* theory data *)
-structure Attributes = TheoryDataFun
+structure Attributes = Theory_Data
(
type T = ((src -> attribute) * string) Name_Space.table;
val empty : T = Name_Space.empty_table "attribute";
- val copy = I;
val extend = I;
- fun merge _ tables : T = Name_Space.merge_tables tables;
+ fun merge data : T = Name_Space.merge_tables data;
);
fun print_attributes thy =
@@ -321,13 +320,12 @@
(* naming *)
-structure Configs = TheoryDataFun
+structure Configs = Theory_Data
(
type T = Config.value Config.T Symtab.table;
val empty = Symtab.empty;
- val copy = I;
val extend = I;
- fun merge _ = Symtab.merge (K true);
+ fun merge data = Symtab.merge (K true) data;
);
fun print_configs ctxt =
--- a/src/Pure/Isar/calculation.ML Sun Nov 08 15:45:09 2009 +0100
+++ b/src/Pure/Isar/calculation.ML Sun Nov 08 20:50:31 2009 +0100
@@ -27,13 +27,12 @@
(** calculation data **)
-structure CalculationData = GenericDataFun
+structure CalculationData = Generic_Data
(
type T = (thm Item_Net.T * thm list) * (thm list * int) option;
val empty = ((Thm.elim_rules, []), NONE);
val extend = I;
-
- fun merge _ (((trans1, sym1), _), ((trans2, sym2), _)) =
+ fun merge (((trans1, sym1), _), ((trans2, sym2), _)) =
((Item_Net.merge (trans1, trans2), Thm.merge_thms (sym1, sym2)), NONE);
);
--- a/src/Pure/Isar/class_target.ML Sun Nov 08 15:45:09 2009 +0100
+++ b/src/Pure/Isar/class_target.ML Sun Nov 08 20:50:31 2009 +0100
@@ -105,13 +105,12 @@
(Thm.merge_thms (defs1, defs2),
AList.merge (op =) (K true) (operations1, operations2)));
-structure ClassData = TheoryDataFun
+structure ClassData = Theory_Data
(
type T = class_data Graph.T
val empty = Graph.empty;
- val copy = I;
val extend = I;
- fun merge _ = Graph.join merge_class_data;
+ val merge = Graph.join merge_class_data;
);
@@ -398,7 +397,7 @@
(*(instantiation parameter, type constructor), (local instantiation parameter, typ)*)
}
-structure Instantiation = ProofDataFun
+structure Instantiation = Proof_Data
(
type T = instantiation
fun init _ = Instantiation { arities = ([], [], []), params = [] };
--- a/src/Pure/Isar/code.ML Sun Nov 08 15:45:09 2009 +0100
+++ b/src/Pure/Isar/code.ML Sun Nov 08 20:50:31 2009 +0100
@@ -703,13 +703,12 @@
(* c.f. src/HOL/Tools/recfun_codegen.ML *)
-structure Code_Target_Attr = TheoryDataFun (
+structure Code_Target_Attr = Theory_Data
+(
type T = (string -> thm -> theory -> theory) option;
val empty = NONE;
- val copy = I;
val extend = I;
- fun merge _ (NONE, f2) = f2
- | merge _ (f1, _) = f1;
+ fun merge (f1, f2) = if is_some f1 then f1 else f2;
);
fun set_code_target_attr f = Code_Target_Attr.map (K (SOME f));
@@ -794,12 +793,12 @@
structure Predicate_Compile_Preproc_Const_Defs : PREDICATE_COMPILE_PREPROC_CONST_DEFS =
struct
-structure Data = GenericDataFun
+structure Data = Generic_Data
(
type T = thm list;
val empty = [];
val extend = I;
- fun merge _ = Thm.merge_thms;
+ val merge = Thm.merge_thms;
);
val get = Data.get o Context.Proof;
--- a/src/Pure/Isar/context_rules.ML Sun Nov 08 15:45:09 2009 +0100
+++ b/src/Pure/Isar/context_rules.ML Sun Nov 08 20:50:31 2009 +0100
@@ -89,13 +89,13 @@
else make_rules next (filter_out eq_th rules) (map (del false o del true) netpairs) wrappers
end;
-structure Rules = GenericDataFun
+structure Rules = Generic_Data
(
type T = rules;
val empty = make_rules ~1 [] empty_netpairs ([], []);
val extend = I;
-
- fun merge _ (Rules {rules = rules1, wrappers = (ws1, ws1'), ...},
+ fun merge
+ (Rules {rules = rules1, wrappers = (ws1, ws1'), ...},
Rules {rules = rules2, wrappers = (ws2, ws2'), ...}) =
let
val wrappers =
--- a/src/Pure/Isar/isar_cmd.ML Sun Nov 08 15:45:09 2009 +0100
+++ b/src/Pure/Isar/isar_cmd.ML Sun Nov 08 20:50:31 2009 +0100
@@ -50,7 +50,7 @@
val print_abbrevs: Toplevel.transition -> Toplevel.transition
val print_facts: Toplevel.transition -> Toplevel.transition
val print_configs: Toplevel.transition -> Toplevel.transition
- val print_theorems: Toplevel.transition -> Toplevel.transition
+ val print_theorems: bool -> Toplevel.transition -> Toplevel.transition
val print_locales: Toplevel.transition -> Toplevel.transition
val print_locale: bool * xstring -> Toplevel.transition -> Toplevel.transition
val print_registrations: string -> Toplevel.transition -> Toplevel.transition
@@ -343,20 +343,20 @@
ProofContext.setmp_verbose_CRITICAL
ProofContext.print_lthms (Proof.context_of (Toplevel.proof_of state)));
-val print_theorems_theory = Toplevel.keep (fn state =>
+fun print_theorems_theory verbose = Toplevel.keep (fn state =>
Toplevel.theory_of state |>
(case Toplevel.previous_context_of state of
- SOME prev => Proof_Display.print_theorems_diff (ProofContext.theory_of prev)
- | NONE => Proof_Display.print_theorems));
+ SOME prev => Proof_Display.print_theorems_diff verbose (ProofContext.theory_of prev)
+ | NONE => Proof_Display.print_theorems verbose));
-val print_theorems = Toplevel.unknown_context o print_theorems_theory o print_theorems_proof;
+fun print_theorems verbose =
+ Toplevel.unknown_context o print_theorems_theory verbose o print_theorems_proof;
val print_locales = Toplevel.unknown_theory o
Toplevel.keep (Locale.print_locales o Toplevel.theory_of);
-fun print_locale (show_facts, name) = Toplevel.unknown_theory o
- Toplevel.keep (fn state =>
- Locale.print_locale (Toplevel.theory_of state) show_facts name);
+fun print_locale (verbose, name) = Toplevel.unknown_theory o
+ Toplevel.keep (fn state => Locale.print_locale (Toplevel.theory_of state) verbose name);
fun print_registrations name = Toplevel.unknown_context o
Toplevel.keep (fn state =>
--- a/src/Pure/Isar/isar_syn.ML Sun Nov 08 15:45:09 2009 +0100
+++ b/src/Pure/Isar/isar_syn.ML Sun Nov 08 20:50:31 2009 +0100
@@ -780,7 +780,7 @@
val _ =
OuterSyntax.improper_command "print_theorems"
"print theorems of local theory or proof context" K.diag
- (Scan.succeed (Toplevel.no_timing o IsarCmd.print_theorems));
+ (opt_bang >> (Toplevel.no_timing oo IsarCmd.print_theorems));
val _ =
OuterSyntax.improper_command "print_locales" "print locales of this theory" K.diag
--- a/src/Pure/Isar/local_defs.ML Sun Nov 08 15:45:09 2009 +0100
+++ b/src/Pure/Isar/local_defs.ML Sun Nov 08 20:50:31 2009 +0100
@@ -186,12 +186,12 @@
(* transformation rules *)
-structure Rules = GenericDataFun
+structure Rules = Generic_Data
(
type T = thm list;
- val empty = []
+ val empty = [];
val extend = I;
- fun merge _ = Thm.merge_thms;
+ val merge = Thm.merge_thms;
);
fun print_rules ctxt =
--- a/src/Pure/Isar/local_theory.ML Sun Nov 08 15:45:09 2009 +0100
+++ b/src/Pure/Isar/local_theory.ML Sun Nov 08 20:50:31 2009 +0100
@@ -85,7 +85,7 @@
(* context data *)
-structure Data = ProofDataFun
+structure Data = Proof_Data
(
type T = lthy option;
fun init _ = NONE;
--- a/src/Pure/Isar/locale.ML Sun Nov 08 15:45:09 2009 +0100
+++ b/src/Pure/Isar/locale.ML Sun Nov 08 20:50:31 2009 +0100
@@ -122,13 +122,12 @@
merge (eq_snd op =) (notes, notes')),
merge (eq_snd op =) (dependencies, dependencies')));
-structure Locales = TheoryDataFun
+structure Locales = Theory_Data
(
type T = locale Name_Space.table;
val empty : T = Name_Space.empty_table "locale";
- val copy = I;
val extend = I;
- fun merge _ = Name_Space.join_tables (K merge_locale);
+ val merge = Name_Space.join_tables (K merge_locale);
);
val intern = Name_Space.intern o #1 o Locales.get;
@@ -188,12 +187,12 @@
datatype 'a delayed = Ready of 'a | ToDo of 'a delayed * 'a delayed;
-structure Identifiers = GenericDataFun
+structure Identifiers = Generic_Data
(
type T = (string * term list) list delayed;
val empty = Ready [];
val extend = I;
- fun merge _ = ToDo;
+ val merge = ToDo;
);
fun finish thy (ToDo (i1, i2)) = merge (ident_eq thy) (finish thy i1, finish thy i2)
@@ -332,7 +331,7 @@
(*** Registrations: interpretations in theories ***)
-structure Registrations = TheoryDataFun
+structure Registrations = Theory_Data
(
type T = ((string * (morphism * morphism)) * stamp) list *
(* registrations, in reverse order of declaration *)
@@ -340,8 +339,7 @@
(* alist of mixin lists, per list mixins in reverse order of declaration *)
val empty = ([], []);
val extend = I;
- val copy = I;
- fun merge _ ((r1, m1), (r2, m2)) : T =
+ fun merge ((r1, m1), (r2, m2)) : T =
(Library.merge (eq_snd op =) (r1, r2),
AList.join (op =) (K (Library.merge (eq_snd op =))) (m1, m2));
(* FIXME consolidate with dependencies, consider one data slot only *)
@@ -569,12 +567,12 @@
(* Storage for witnesses, intro and unfold rules *)
-structure Thms = GenericDataFun
+structure Thms = Generic_Data
(
type T = thm list * thm list * thm list;
val empty = ([], [], []);
val extend = I;
- fun merge _ ((witnesses1, intros1, unfolds1), (witnesses2, intros2, unfolds2)) =
+ fun merge ((witnesses1, intros1, unfolds1), (witnesses2, intros2, unfolds2)) =
(Thm.merge_thms (witnesses1, witnesses2),
Thm.merge_thms (intros1, intros2),
Thm.merge_thms (unfolds1, unfolds2));
--- a/src/Pure/Isar/method.ML Sun Nov 08 15:45:09 2009 +0100
+++ b/src/Pure/Isar/method.ML Sun Nov 08 20:50:31 2009 +0100
@@ -270,7 +270,7 @@
(* ML tactics *)
-structure TacticData = ProofDataFun
+structure TacticData = Proof_Data
(
type T = thm list -> tactic;
fun init _ = undefined;
@@ -320,13 +320,12 @@
(* method definitions *)
-structure Methods = TheoryDataFun
+structure Methods = Theory_Data
(
type T = ((src -> Proof.context -> method) * string) Name_Space.table;
val empty : T = Name_Space.empty_table "method";
- val copy = I;
val extend = I;
- fun merge _ tables : T = Name_Space.merge_tables tables;
+ fun merge data : T = Name_Space.merge_tables data;
);
fun print_methods thy =
--- a/src/Pure/Isar/object_logic.ML Sun Nov 08 15:45:09 2009 +0100
+++ b/src/Pure/Isar/object_logic.ML Sun Nov 08 20:50:31 2009 +0100
@@ -47,18 +47,17 @@
fun make_data (base_sort, judgment, atomize_rulify) =
Data {base_sort = base_sort, judgment = judgment, atomize_rulify = atomize_rulify};
-structure ObjectLogicData = TheoryDataFun
+structure ObjectLogicData = Theory_Data
(
type T = data;
val empty = make_data (NONE, NONE, ([], []));
- val copy = I;
val extend = I;
fun merge_opt eq (SOME x, SOME y) =
if eq (x, y) then SOME x else error "Attempt to merge different object-logics"
| merge_opt _ (x, y) = if is_some x then x else y;
- fun merge _
+ fun merge
(Data {base_sort = base_sort1, judgment = judgment1, atomize_rulify = (atomize1, rulify1)},
Data {base_sort = base_sort2, judgment = judgment2, atomize_rulify = (atomize2, rulify2)}) =
make_data (merge_opt (op =) (base_sort1, base_sort2), merge_opt (op =) (judgment1, judgment2),
--- a/src/Pure/Isar/overloading.ML Sun Nov 08 15:45:09 2009 +0100
+++ b/src/Pure/Isar/overloading.ML Sun Nov 08 20:50:31 2009 +0100
@@ -30,7 +30,8 @@
((((string * typ -> (typ * typ) option) * (string * typ -> (typ * term) option)) * bool) *
(term * term) list)) * bool);
-structure ImprovableSyntax = ProofDataFun(
+structure ImprovableSyntax = Proof_Data
+(
type T = {
primary_constraints: (string * typ) list,
secondary_constraints: (string * typ) list,
@@ -119,7 +120,7 @@
(* bookkeeping *)
-structure OverloadingData = ProofDataFun
+structure OverloadingData = Proof_Data
(
type T = ((string * typ) * (string * bool)) list;
fun init _ = [];
--- a/src/Pure/Isar/proof_context.ML Sun Nov 08 15:45:09 2009 +0100
+++ b/src/Pure/Isar/proof_context.ML Sun Nov 08 20:50:31 2009 +0100
@@ -177,7 +177,7 @@
val local_naming = Name_Space.default_naming |> Name_Space.add_path "local";
-structure ContextData = ProofDataFun
+structure ContextData = Proof_Data
(
type T = ctxt;
fun init thy =
@@ -515,7 +515,7 @@
local
-structure Allow_Dummies = ProofDataFun(type T = bool fun init _ = false);
+structure Allow_Dummies = Proof_Data(type T = bool fun init _ = false);
fun check_dummies ctxt t =
if Allow_Dummies.get ctxt then t
--- a/src/Pure/Isar/proof_display.ML Sun Nov 08 15:45:09 2009 +0100
+++ b/src/Pure/Isar/proof_display.ML Sun Nov 08 20:50:31 2009 +0100
@@ -12,8 +12,8 @@
val pp_term: theory -> term -> Pretty.T
val pp_ctyp: ctyp -> Pretty.T
val pp_cterm: cterm -> Pretty.T
- val print_theorems_diff: theory -> theory -> unit
- val print_theorems: theory -> unit
+ val print_theorems_diff: bool -> theory -> theory -> unit
+ val print_theorems: bool -> theory -> unit
val pretty_full_theory: bool -> theory -> Pretty.T
val print_theory: theory -> unit
val string_of_rule: Proof.context -> string -> thm -> string
@@ -46,20 +46,23 @@
(* theorems and theory *)
-fun pretty_theorems_diff prev_thys thy =
+fun pretty_theorems_diff verbose prev_thys thy =
let
val pretty_fact = ProofContext.pretty_fact (ProofContext.init thy);
- val thmss = Facts.dest_static (map PureThy.facts_of prev_thys) (PureThy.facts_of thy);
+ val facts = PureThy.facts_of thy;
+ val thmss =
+ Facts.dest_static (map PureThy.facts_of prev_thys) facts
+ |> not verbose ? filter_out (Facts.is_concealed facts o #1);
in Pretty.big_list "theorems:" (map #1 (sort_wrt (#1 o #2) (map (`pretty_fact) thmss))) end;
-fun print_theorems_diff prev_thy thy =
- Pretty.writeln (pretty_theorems_diff [prev_thy] thy);
+fun print_theorems_diff verbose prev_thy thy =
+ Pretty.writeln (pretty_theorems_diff verbose [prev_thy] thy);
-fun pretty_theorems thy = pretty_theorems_diff (Theory.parents_of thy) thy;
-val print_theorems = Pretty.writeln o pretty_theorems;
+fun pretty_theorems verbose thy = pretty_theorems_diff verbose (Theory.parents_of thy) thy;
+val print_theorems = Pretty.writeln oo pretty_theorems;
fun pretty_full_theory verbose thy =
- Pretty.chunks (Display.pretty_full_theory verbose thy @ [pretty_theorems thy]);
+ Pretty.chunks (Display.pretty_full_theory verbose thy @ [pretty_theorems verbose thy]);
val print_theory = Pretty.writeln o pretty_full_theory false;
--- a/src/Pure/Isar/spec_rules.ML Sun Nov 08 15:45:09 2009 +0100
+++ b/src/Pure/Isar/spec_rules.ML Sun Nov 08 20:50:31 2009 +0100
@@ -24,7 +24,7 @@
datatype rough_classification = Unknown | Equational | Inductive | Co_Inductive;
type spec = rough_classification * (term list * thm list);
-structure Rules = GenericDataFun
+structure Rules = Generic_Data
(
type T = spec Item_Net.T;
val empty : T =
@@ -35,7 +35,7 @@
eq_list Thm.eq_thm_prop (ths1, ths2))
(#1 o #2);
val extend = I;
- fun merge _ = Item_Net.merge;
+ fun merge data = Item_Net.merge data;
);
val get = Item_Net.content o Rules.get o Context.Proof;
--- a/src/Pure/Isar/specification.ML Sun Nov 08 15:45:09 2009 +0100
+++ b/src/Pure/Isar/specification.ML Sun Nov 08 20:50:31 2009 +0100
@@ -333,12 +333,12 @@
[((Binding.name Obtain.thatN, []), [(ths, [])])] #> #2 #> pair ths);
in ((prems, stmt, SOME facts), goal_ctxt) end);
-structure TheoremHook = GenericDataFun
+structure TheoremHook = Generic_Data
(
type T = ((bool -> Proof.state -> Proof.state) * stamp) list;
val empty = [];
val extend = I;
- fun merge _ hooks : T = Library.merge (eq_snd op =) hooks;
+ fun merge hooks : T = Library.merge (eq_snd op =) hooks;
);
fun gen_theorem prep_att prep_stmt
--- a/src/Pure/Isar/theory_target.ML Sun Nov 08 15:45:09 2009 +0100
+++ b/src/Pure/Isar/theory_target.ML Sun Nov 08 20:50:31 2009 +0100
@@ -34,7 +34,7 @@
val global_target = make_target "" false false ([], [], []) [];
-structure Data = ProofDataFun
+structure Data = Proof_Data
(
type T = target;
fun init _ = global_target;
--- a/src/Pure/Isar/toplevel.ML Sun Nov 08 15:45:09 2009 +0100
+++ b/src/Pure/Isar/toplevel.ML Sun Nov 08 20:50:31 2009 +0100
@@ -631,7 +631,7 @@
(* excursion of units, consisting of commands with proof *)
-structure States = ProofDataFun
+structure States = Proof_Data
(
type T = state list future option;
fun init _ = NONE;
--- a/src/Pure/ML/ml_antiquote.ML Sun Nov 08 15:45:09 2009 +0100
+++ b/src/Pure/ML/ml_antiquote.ML Sun Nov 08 20:50:31 2009 +0100
@@ -20,7 +20,7 @@
(* ML names *)
-structure NamesData = ProofDataFun
+structure NamesData = Proof_Data
(
type T = Name.context;
fun init _ = ML_Syntax.reserved;
--- a/src/Pure/ML/ml_env.ML Sun Nov 08 15:45:09 2009 +0100
+++ b/src/Pure/ML/ml_env.ML Sun Nov 08 20:50:31 2009 +0100
@@ -16,7 +16,7 @@
(* context data *)
-structure Env = GenericDataFun
+structure Env = Generic_Data
(
type T =
ML_Name_Space.valueVal Symtab.table *
@@ -27,7 +27,7 @@
ML_Name_Space.functorVal Symtab.table;
val empty = (Symtab.empty, Symtab.empty, Symtab.empty, Symtab.empty, Symtab.empty, Symtab.empty);
val extend = I;
- fun merge _
+ fun merge
((val1, type1, fixity1, structure1, signature1, functor1),
(val2, type2, fixity2, structure2, signature2, functor2)) : T =
(Symtab.merge (K true) (val1, val2),
--- a/src/Pure/ML/ml_thms.ML Sun Nov 08 15:45:09 2009 +0100
+++ b/src/Pure/ML/ml_thms.ML Sun Nov 08 20:50:31 2009 +0100
@@ -15,7 +15,7 @@
(* auxiliary facts table *)
-structure AuxFacts = ProofDataFun
+structure AuxFacts = Proof_Data
(
type T = thm list Inttab.table;
fun init _ = Inttab.empty;
--- a/src/Pure/Proof/extraction.ML Sun Nov 08 15:45:09 2009 +0100
+++ b/src/Pure/Proof/extraction.ML Sun Nov 08 20:50:31 2009 +0100
@@ -167,7 +167,7 @@
(* theory data *)
-structure ExtractionData = TheoryDataFun
+structure ExtractionData = Theory_Data
(
type T =
{realizes_eqns : rules,
@@ -187,20 +187,19 @@
defs = [],
expand = [],
prep = NONE};
- val copy = I;
val extend = I;
- fun merge _
- (({realizes_eqns = realizes_eqns1, typeof_eqns = typeof_eqns1, types = types1,
+ fun merge
+ ({realizes_eqns = realizes_eqns1, typeof_eqns = typeof_eqns1, types = types1,
realizers = realizers1, defs = defs1, expand = expand1, prep = prep1},
{realizes_eqns = realizes_eqns2, typeof_eqns = typeof_eqns2, types = types2,
- realizers = realizers2, defs = defs2, expand = expand2, prep = prep2}) : T * T) =
+ realizers = realizers2, defs = defs2, expand = expand2, prep = prep2}) : T =
{realizes_eqns = merge_rules realizes_eqns1 realizes_eqns2,
typeof_eqns = merge_rules typeof_eqns1 typeof_eqns2,
types = AList.merge (op =) (K true) (types1, types2),
realizers = Symtab.merge_list (eq_set (op =) o pairself #1) (realizers1, realizers2),
defs = Library.merge Thm.eq_thm (defs1, defs2),
- expand = Library.merge (op =) (expand1, expand2),
+ expand = Library.merge (op =) (expand1, expand2), (* FIXME proper aconv !?! *)
prep = (case prep1 of NONE => prep2 | _ => prep1)};
);
--- a/src/Pure/Syntax/syntax.ML Sun Nov 08 15:45:09 2009 +0100
+++ b/src/Pure/Syntax/syntax.ML Sun Nov 08 20:50:31 2009 +0100
@@ -741,14 +741,14 @@
type key = int * bool;
type 'a check = 'a list -> Proof.context -> ('a list * Proof.context) option;
-structure Checks = GenericDataFun
+structure Checks = Generic_Data
(
type T =
((key * ((string * typ check) * stamp) list) list *
(key * ((string * term check) * stamp) list) list);
val empty = ([], []);
val extend = I;
- fun merge _ ((typ_checks1, term_checks1), (typ_checks2, term_checks2)) : T =
+ fun merge ((typ_checks1, term_checks1), (typ_checks2, term_checks2)) : T =
(AList.join (op =) (K (Library.merge (eq_snd (op =)))) (typ_checks1, typ_checks2),
AList.join (op =) (K (Library.merge (eq_snd (op =)))) (term_checks1, term_checks2));
);
@@ -877,7 +877,7 @@
(* global pretty printing *)
-structure PrettyGlobal = ProofDataFun(type T = bool fun init _ = false);
+structure PrettyGlobal = Proof_Data(type T = bool fun init _ = false);
val is_pretty_global = PrettyGlobal.get;
val set_pretty_global = PrettyGlobal.put;
val init_pretty_global = set_pretty_global true o ProofContext.init;
--- a/src/Pure/Thy/present.ML Sun Nov 08 15:45:09 2009 +0100
+++ b/src/Pure/Thy/present.ML Sun Nov 08 20:50:31 2009 +0100
@@ -64,13 +64,12 @@
(** additional theory data **)
-structure BrowserInfoData = TheoryDataFun
+structure BrowserInfoData = Theory_Data
(
type T = {name: string, session: string list, is_local: bool};
val empty = {name = "", session = [], is_local = false}: T;
- val copy = I;
fun extend _ = empty;
- fun merge _ _ = empty;
+ fun merge _ = empty;
);
val put_info = BrowserInfoData.put;
--- a/src/Pure/Thy/term_style.ML Sun Nov 08 15:45:09 2009 +0100
+++ b/src/Pure/Thy/term_style.ML Sun Nov 08 20:50:31 2009 +0100
@@ -19,13 +19,12 @@
fun err_dup_style name =
error ("Duplicate declaration of antiquote style: " ^ quote name);
-structure StyleData = TheoryDataFun
+structure StyleData = Theory_Data
(
type T = ((Proof.context -> term -> term) parser * stamp) Symtab.table;
val empty = Symtab.empty;
- val copy = I;
val extend = I;
- fun merge _ tabs : T = Symtab.merge (eq_snd (op =)) tabs
+ fun merge data : T = Symtab.merge (eq_snd (op =)) data
handle Symtab.DUP dup => err_dup_style dup;
);
--- a/src/Pure/Thy/thy_info.ML Sun Nov 08 15:45:09 2009 +0100
+++ b/src/Pure/Thy/thy_info.ML Sun Nov 08 20:50:31 2009 +0100
@@ -233,15 +233,14 @@
(* management data *)
-structure Management_Data = TheoryDataFun
+structure Management_Data = Theory_Data
(
type T =
Task_Queue.group option * (*worker thread group*)
int; (*abstract update time*)
val empty = (NONE, 0);
- val copy = I;
fun extend _ = empty;
- fun merge _ _ = empty;
+ fun merge _ = empty;
);
val thy_ord = int_ord o pairself (#2 o Management_Data.get);
--- a/src/Pure/Tools/named_thms.ML Sun Nov 08 15:45:09 2009 +0100
+++ b/src/Pure/Tools/named_thms.ML Sun Nov 08 20:50:31 2009 +0100
@@ -17,12 +17,12 @@
functor Named_Thms(val name: string val description: string): NAMED_THMS =
struct
-structure Data = GenericDataFun
+structure Data = Generic_Data
(
type T = thm Item_Net.T;
val empty = Thm.full_rules;
val extend = I;
- fun merge _ = Item_Net.merge;
+ val merge = Item_Net.merge;
);
val content = Item_Net.content o Data.get;
--- a/src/Pure/assumption.ML Sun Nov 08 15:45:09 2009 +0100
+++ b/src/Pure/assumption.ML Sun Nov 08 20:50:31 2009 +0100
@@ -60,7 +60,7 @@
fun make_data (assms, prems) = Data {assms = assms, prems = prems};
-structure Data = ProofDataFun
+structure Data = Proof_Data
(
type T = data;
fun init _ = make_data ([], []);
--- a/src/Pure/codegen.ML Sun Nov 08 15:45:09 2009 +0100
+++ b/src/Pure/codegen.ML Sun Nov 08 20:50:31 2009 +0100
@@ -185,7 +185,7 @@
(* theory data *)
-structure CodegenData = TheoryDataFun
+structure CodegenData = Theory_Data
(
type T =
{codegens : (string * term codegen) list,
@@ -198,16 +198,15 @@
val empty =
{codegens = [], tycodegens = [], consts = [], types = [],
preprocs = [], modules = Symtab.empty};
- val copy = I;
val extend = I;
- fun merge _
+ fun merge
({codegens = codegens1, tycodegens = tycodegens1,
consts = consts1, types = types1,
preprocs = preprocs1, modules = modules1} : T,
{codegens = codegens2, tycodegens = tycodegens2,
consts = consts2, types = types2,
- preprocs = preprocs2, modules = modules2}) =
+ preprocs = preprocs2, modules = modules2}) : T =
{codegens = AList.merge (op =) (K true) (codegens1, codegens2),
tycodegens = AList.merge (op =) (K true) (tycodegens1, tycodegens2),
consts = AList.merge (op =) (K true) (consts1, consts2),
@@ -287,13 +286,12 @@
| _ => err ()
end;
-structure UnfoldData = TheoryDataFun
+structure UnfoldData = Theory_Data
(
type T = simpset;
val empty = empty_ss;
- val copy = I;
val extend = I;
- fun merge _ = merge_ss;
+ val merge = merge_ss;
);
val map_unfold = UnfoldData.map;
--- a/src/Pure/config.ML Sun Nov 08 15:45:09 2009 +0100
+++ b/src/Pure/config.ML Sun Nov 08 20:50:31 2009 +0100
@@ -90,12 +90,12 @@
(* context information *)
-structure Value = GenericDataFun
+structure Value = Generic_Data
(
type T = value Inttab.table;
val empty = Inttab.empty;
val extend = I;
- fun merge _ = Inttab.merge (K true);
+ fun merge data = Inttab.merge (K true) data;
);
fun declare global name default =
--- a/src/Pure/context.ML Sun Nov 08 15:45:09 2009 +0100
+++ b/src/Pure/context.ML Sun Nov 08 20:50:31 2009 +0100
@@ -572,7 +572,7 @@
(** theory data **)
-signature THEORY_DATA_ARGS =
+signature OLD_THEORY_DATA_ARGS =
sig
type T
val empty: T
@@ -581,7 +581,7 @@
val merge: Pretty.pp -> T * T -> T
end;
-signature THEORY_DATA =
+signature OLD_THEORY_DATA =
sig
type T
val get: theory -> T
@@ -590,7 +590,7 @@
val init: theory -> theory
end;
-functor TheoryDataFun(Data: THEORY_DATA_ARGS): THEORY_DATA =
+functor TheoryDataFun(Data: OLD_THEORY_DATA_ARGS): OLD_THEORY_DATA =
struct
type T = Data.T;
@@ -610,6 +610,38 @@
end;
+signature THEORY_DATA_ARGS =
+sig
+ type T
+ val empty: T
+ val extend: T -> T
+ val merge: T * T -> T
+end;
+
+signature THEORY_DATA =
+sig
+ type T
+ val get: theory -> T
+ val put: T -> theory -> theory
+ val map: (T -> T) -> theory -> theory
+end;
+
+functor Theory_Data(Data: THEORY_DATA_ARGS): THEORY_DATA =
+struct
+
+structure Result = TheoryDataFun
+(
+ type T = Data.T;
+ val empty = Data.empty;
+ val copy = I;
+ val extend = Data.extend;
+ fun merge _ = Data.merge;
+);
+
+open Result;
+
+end;
+
(** proof data **)
@@ -628,7 +660,7 @@
val map: (T -> T) -> Proof.context -> Proof.context
end;
-functor ProofDataFun(Data: PROOF_DATA_ARGS): PROOF_DATA =
+functor Proof_Data(Data: PROOF_DATA_ARGS): PROOF_DATA =
struct
type T = Data.T;
@@ -651,7 +683,7 @@
type T
val empty: T
val extend: T -> T
- val merge: Pretty.pp -> T * T -> T
+ val merge: T * T -> T
end;
signature GENERIC_DATA =
@@ -662,11 +694,11 @@
val map: (T -> T) -> Context.generic -> Context.generic
end;
-functor GenericDataFun(Data: GENERIC_DATA_ARGS): GENERIC_DATA =
+functor Generic_Data(Data: GENERIC_DATA_ARGS): GENERIC_DATA =
struct
-structure Thy_Data = TheoryDataFun(open Data val copy = I);
-structure Prf_Data = ProofDataFun(type T = Data.T val init = Thy_Data.get);
+structure Thy_Data = Theory_Data(Data);
+structure Prf_Data = Proof_Data(type T = Data.T val init = Thy_Data.get);
type T = Data.T;
--- a/src/Pure/context_position.ML Sun Nov 08 15:45:09 2009 +0100
+++ b/src/Pure/context_position.ML Sun Nov 08 20:50:31 2009 +0100
@@ -15,7 +15,7 @@
structure Context_Position: CONTEXT_POSITION =
struct
-structure Data = ProofDataFun
+structure Data = Proof_Data
(
type T = bool;
fun init _ = true;
--- a/src/Pure/interpretation.ML Sun Nov 08 15:45:09 2009 +0100
+++ b/src/Pure/interpretation.ML Sun Nov 08 20:50:31 2009 +0100
@@ -18,13 +18,12 @@
type T = T;
-structure Interp = TheoryDataFun
+structure Interp = Theory_Data
(
type T = T list * (((T -> theory -> theory) * stamp) * T list) list;
val empty = ([], []);
val extend = I;
- val copy = I;
- fun merge _ ((data1, interps1), (data2, interps2)) : T =
+ fun merge ((data1, interps1), (data2, interps2)) : T =
(Library.merge eq (data1, data2),
AList.join (eq_snd (op =)) (K (Library.merge eq)) (interps1, interps2));
);
--- a/src/Pure/meta_simplifier.ML Sun Nov 08 15:45:09 2009 +0100
+++ b/src/Pure/meta_simplifier.ML Sun Nov 08 20:50:31 2009 +0100
@@ -772,7 +772,7 @@
loop_tacs = loop_tacs2, solvers = (unsafe_solvers2, solvers2)}) = ss2;
val rules' = Net.merge eq_rrule (rules1, rules2);
- val prems' = merge Thm.eq_thm_prop (prems1, prems2);
+ val prems' = Thm.merge_thms (prems1, prems2);
val bounds' = if #1 bounds1 < #1 bounds2 then bounds2 else bounds1;
val depth' = if #1 depth1 < #1 depth2 then depth2 else depth1;
val congs' = merge (Thm.eq_thm_prop o pairself #2) (congs1, congs2);
--- a/src/Pure/proofterm.ML Sun Nov 08 15:45:09 2009 +0100
+++ b/src/Pure/proofterm.ML Sun Nov 08 20:50:31 2009 +0100
@@ -1247,14 +1247,13 @@
(**** theory data ****)
-structure ProofData = TheoryDataFun
+structure ProofData = Theory_Data
(
type T = (stamp * (proof * proof)) list * (stamp * (typ list -> proof -> proof option)) list;
val empty = ([], []);
- val copy = I;
val extend = I;
- fun merge _ ((rules1, procs1), (rules2, procs2)) : T =
+ fun merge ((rules1, procs1), (rules2, procs2)) : T =
(AList.merge (op =) (K true) (rules1, rules2),
AList.merge (op =) (K true) (procs1, procs2));
);
--- a/src/Pure/pure_thy.ML Sun Nov 08 15:45:09 2009 +0100
+++ b/src/Pure/pure_thy.ML Sun Nov 08 20:50:31 2009 +0100
@@ -54,13 +54,12 @@
(** theory data **)
-structure FactsData = TheoryDataFun
+structure FactsData = Theory_Data
(
type T = Facts.T * thm list;
val empty = (Facts.empty, []);
- val copy = I;
fun extend (facts, _) = (facts, []);
- fun merge _ ((facts1, _), (facts2, _)) = (Facts.merge (facts1, facts2), []);
+ fun merge ((facts1, _), (facts2, _)) = (Facts.merge (facts1, facts2), []);
);
@@ -246,13 +245,12 @@
("_applC", typ "('b => 'a) => cargs => logic", Mixfix ("(1_/ _)", [1000, 1000], 999)),
("_applC", typ "('b => 'a) => cargs => aprop", Mixfix ("(1_/ _)", [1000, 1000], 999))];
-structure OldApplSyntax = TheoryDataFun
+structure OldApplSyntax = Theory_Data
(
type T = bool;
val empty = false;
- val copy = I;
val extend = I;
- fun merge _ (b1, b2) : T =
+ fun merge (b1, b2) : T =
if b1 = b2 then b1
else error "Cannot merge theories with different application syntax";
);
@@ -269,7 +267,7 @@
val _ = Context.>> (Context.map_theory
(Sign.map_naming (Name_Space.set_theory_name Context.PureN) #>
- OldApplSyntax.init #>
+ OldApplSyntax.put false #>
Sign.add_types
[(Binding.name "fun", 2, NoSyn),
(Binding.name "prop", 0, NoSyn),
--- a/src/Pure/simplifier.ML Sun Nov 08 15:45:09 2009 +0100
+++ b/src/Pure/simplifier.ML Sun Nov 08 20:50:31 2009 +0100
@@ -99,12 +99,12 @@
(** simpset data **)
-structure SimpsetData = GenericDataFun
+structure SimpsetData = Generic_Data
(
type T = simpset;
val empty = empty_ss;
fun extend ss = MetaSimplifier.inherit_context empty_ss ss;
- fun merge _ = merge_ss;
+ val merge = merge_ss;
);
val get_ss = SimpsetData.get;
@@ -145,12 +145,12 @@
(* data *)
-structure Simprocs = GenericDataFun
+structure Simprocs = Generic_Data
(
type T = simproc Name_Space.table;
val empty : T = Name_Space.empty_table "simproc";
val extend = I;
- fun merge _ simprocs = Name_Space.merge_tables simprocs;
+ fun merge simprocs = Name_Space.merge_tables simprocs;
);
--- a/src/Pure/thm.ML Sun Nov 08 15:45:09 2009 +0100
+++ b/src/Pure/thm.ML Sun Nov 08 20:50:31 2009 +0100
@@ -1724,13 +1724,12 @@
(* authentic derivation names *)
-structure Oracles = TheoryDataFun
+structure Oracles = Theory_Data
(
type T = unit Name_Space.table;
val empty : T = Name_Space.empty_table "oracle";
- val copy = I;
val extend = I;
- fun merge _ oracles : T = Name_Space.merge_tables oracles;
+ fun merge data : T = Name_Space.merge_tables data;
);
val extern_oracles = map #1 o Name_Space.extern_table o Oracles.get;
--- a/src/Pure/type.ML Sun Nov 08 15:45:09 2009 +0100
+++ b/src/Pure/type.ML Sun Nov 08 20:50:31 2009 +0100
@@ -147,7 +147,7 @@
val mode_syntax = Mode {normalize = true, logical = false};
val mode_abbrev = Mode {normalize = false, logical = false};
-structure Mode = ProofDataFun
+structure Mode = Proof_Data
(
type T = mode;
fun init _ = mode_default;
--- a/src/Pure/variable.ML Sun Nov 08 15:45:09 2009 +0100
+++ b/src/Pure/variable.ML Sun Nov 08 20:50:31 2009 +0100
@@ -86,7 +86,7 @@
Data {is_body = is_body, names = names, consts = consts, fixes = fixes, binds = binds,
type_occs = type_occs, maxidx = maxidx, sorts = sorts, constraints = constraints};
-structure Data = ProofDataFun
+structure Data = Proof_Data
(
type T = data;
fun init _ =
--- a/src/Tools/Code/code_ml.ML Sun Nov 08 15:45:09 2009 +0100
+++ b/src/Tools/Code/code_ml.ML Sun Nov 08 20:50:31 2009 +0100
@@ -947,7 +947,7 @@
local
-structure CodeAntiqData = ProofDataFun
+structure CodeAntiqData = Proof_Data
(
type T = (string list * string list) * (bool * (string
* (string * ((string * string) list * (string * string) list)) lazy));
--- a/src/Tools/Code/code_preproc.ML Sun Nov 08 15:45:09 2009 +0100
+++ b/src/Tools/Code/code_preproc.ML Sun Nov 08 20:50:31 2009 +0100
@@ -56,13 +56,12 @@
val functrans = AList.merge (op =) (eq_fst (op =)) (functrans1, functrans2);
in make_thmproc ((pre, post), functrans) end;
-structure Code_Preproc_Data = TheoryDataFun
+structure Code_Preproc_Data = Theory_Data
(
type T = thmproc;
val empty = make_thmproc ((Simplifier.empty_ss, Simplifier.empty_ss), []);
- fun copy spec = spec;
- val extend = copy;
- fun merge _ = merge_thmproc;
+ val extend = I;
+ val merge = merge_thmproc;
);
fun the_thmproc thy = case Code_Preproc_Data.get thy
--- a/src/Tools/Code/code_target.ML Sun Nov 08 15:45:09 2009 +0100
+++ b/src/Tools/Code/code_target.ML Sun Nov 08 20:50:31 2009 +0100
@@ -148,13 +148,12 @@
else
error ("Incompatible serializers: " ^ quote target);
-structure CodeTargetData = TheoryDataFun
+structure CodeTargetData = Theory_Data
(
type T = target Symtab.table * string list;
val empty = (Symtab.empty, []);
- val copy = I;
val extend = I;
- fun merge _ ((target1, exc1) : T, (target2, exc2)) =
+ fun merge ((target1, exc1), (target2, exc2)) : T =
(Symtab.join (merge_target true) (target1, target2), Library.merge (op =) (exc1, exc2));
);
--- a/src/Tools/Metis/metis.ML Sun Nov 08 15:45:09 2009 +0100
+++ b/src/Tools/Metis/metis.ML Sun Nov 08 20:50:31 2009 +0100
@@ -60,7 +60,7 @@
structure Metis = struct open Metis
(* Metis-specific ML environment *)
-nonfix ++ -- RL mem union subset;
+nonfix ++ -- RL mem;
val explode = String.explode;
val implode = String.implode;
val print = TextIO.print;
@@ -102,10 +102,10 @@
(* Generating random values. *)
(* ------------------------------------------------------------------------- *)
-val randomWord = RandomWord.next_word;
-val randomBool = RandomWord.next_bool;
-fun randomInt n = RandomWord.next_int 0 (n - 1);
-val randomReal = RandomWord.next_real;
+val randomWord = Random_Word.next_word;
+val randomBool = Random_Word.next_bool;
+fun randomInt n = Random_Word.next_int 0 (n - 1);
+val randomReal = Random_Word.next_real;
end;
@@ -347,7 +347,7 @@
structure Metis = struct open Metis
(* Metis-specific ML environment *)
-nonfix ++ -- RL mem union subset;
+nonfix ++ -- RL mem;
val explode = String.explode;
val implode = String.implode;
val print = TextIO.print;
@@ -1274,7 +1274,7 @@
structure Metis = struct open Metis
(* Metis-specific ML environment *)
-nonfix ++ -- RL mem union subset;
+nonfix ++ -- RL mem;
val explode = String.explode;
val implode = String.implode;
val print = TextIO.print;
@@ -1979,7 +1979,7 @@
structure Metis = struct open Metis
(* Metis-specific ML environment *)
-nonfix ++ -- RL mem union subset;
+nonfix ++ -- RL mem;
val explode = String.explode;
val implode = String.implode;
val print = TextIO.print;
@@ -2061,7 +2061,7 @@
structure Metis = struct open Metis
(* Metis-specific ML environment *)
-nonfix ++ -- RL mem union subset;
+nonfix ++ -- RL mem;
val explode = String.explode;
val implode = String.implode;
val print = TextIO.print;
@@ -2200,7 +2200,7 @@
structure Metis = struct open Metis
(* Metis-specific ML environment *)
-nonfix ++ -- RL mem union subset;
+nonfix ++ -- RL mem;
val explode = String.explode;
val implode = String.implode;
val print = TextIO.print;
@@ -2820,7 +2820,7 @@
structure Metis = struct open Metis
(* Metis-specific ML environment *)
-nonfix ++ -- RL mem union subset;
+nonfix ++ -- RL mem;
val explode = String.explode;
val implode = String.implode;
val print = TextIO.print;
@@ -3187,7 +3187,7 @@
structure Metis = struct open Metis
(* Metis-specific ML environment *)
-nonfix ++ -- RL mem union subset;
+nonfix ++ -- RL mem;
val explode = String.explode;
val implode = String.implode;
val print = TextIO.print;
@@ -3823,7 +3823,7 @@
structure Metis = struct open Metis
(* Metis-specific ML environment *)
-nonfix ++ -- RL mem union subset;
+nonfix ++ -- RL mem;
val explode = String.explode;
val implode = String.implode;
val print = TextIO.print;
@@ -4106,7 +4106,7 @@
structure Metis = struct open Metis
(* Metis-specific ML environment *)
-nonfix ++ -- RL mem union subset;
+nonfix ++ -- RL mem;
val explode = String.explode;
val implode = String.implode;
val print = TextIO.print;
@@ -4297,7 +4297,7 @@
structure Metis = struct open Metis
(* Metis-specific ML environment *)
-nonfix ++ -- RL mem union subset;
+nonfix ++ -- RL mem;
val explode = String.explode;
val implode = String.implode;
val print = TextIO.print;
@@ -4550,7 +4550,7 @@
structure Metis = struct open Metis
(* Metis-specific ML environment *)
-nonfix ++ -- RL mem union subset;
+nonfix ++ -- RL mem;
val explode = String.explode;
val implode = String.implode;
val print = TextIO.print;
@@ -4787,7 +4787,7 @@
structure Metis = struct open Metis
(* Metis-specific ML environment *)
-nonfix ++ -- RL mem union subset;
+nonfix ++ -- RL mem;
val explode = String.explode;
val implode = String.implode;
val print = TextIO.print;
@@ -5293,7 +5293,7 @@
structure Metis = struct open Metis
(* Metis-specific ML environment *)
-nonfix ++ -- RL mem union subset;
+nonfix ++ -- RL mem;
val explode = String.explode;
val implode = String.implode;
val print = TextIO.print;
@@ -5565,7 +5565,7 @@
structure Metis = struct open Metis
(* Metis-specific ML environment *)
-nonfix ++ -- RL mem union subset;
+nonfix ++ -- RL mem;
val explode = String.explode;
val implode = String.implode;
val print = TextIO.print;
@@ -5843,7 +5843,7 @@
structure Metis = struct open Metis
(* Metis-specific ML environment *)
-nonfix ++ -- RL mem union subset;
+nonfix ++ -- RL mem;
val explode = String.explode;
val implode = String.implode;
val print = TextIO.print;
@@ -6622,7 +6622,7 @@
structure Metis = struct open Metis
(* Metis-specific ML environment *)
-nonfix ++ -- RL mem union subset;
+nonfix ++ -- RL mem;
val explode = String.explode;
val implode = String.implode;
val print = TextIO.print;
@@ -6983,7 +6983,7 @@
structure Metis = struct open Metis
(* Metis-specific ML environment *)
-nonfix ++ -- RL mem union subset;
+nonfix ++ -- RL mem;
val explode = String.explode;
val implode = String.implode;
val print = TextIO.print;
@@ -7423,7 +7423,7 @@
structure Metis = struct open Metis
(* Metis-specific ML environment *)
-nonfix ++ -- RL mem union subset;
+nonfix ++ -- RL mem;
val explode = String.explode;
val implode = String.implode;
val print = TextIO.print;
@@ -8117,7 +8117,7 @@
structure Metis = struct open Metis
(* Metis-specific ML environment *)
-nonfix ++ -- RL mem union subset;
+nonfix ++ -- RL mem;
val explode = String.explode;
val implode = String.implode;
val print = TextIO.print;
@@ -8554,7 +8554,7 @@
structure Metis = struct open Metis
(* Metis-specific ML environment *)
-nonfix ++ -- RL mem union subset;
+nonfix ++ -- RL mem;
val explode = String.explode;
val implode = String.implode;
val print = TextIO.print;
@@ -8846,7 +8846,7 @@
structure Metis = struct open Metis
(* Metis-specific ML environment *)
-nonfix ++ -- RL mem union subset;
+nonfix ++ -- RL mem;
val explode = String.explode;
val implode = String.implode;
val print = TextIO.print;
@@ -9521,7 +9521,7 @@
structure Metis = struct open Metis
(* Metis-specific ML environment *)
-nonfix ++ -- RL mem union subset;
+nonfix ++ -- RL mem;
val explode = String.explode;
val implode = String.implode;
val print = TextIO.print;
@@ -10321,7 +10321,7 @@
structure Metis = struct open Metis
(* Metis-specific ML environment *)
-nonfix ++ -- RL mem union subset;
+nonfix ++ -- RL mem;
val explode = String.explode;
val implode = String.implode;
val print = TextIO.print;
@@ -11493,7 +11493,7 @@
structure Metis = struct open Metis
(* Metis-specific ML environment *)
-nonfix ++ -- RL mem union subset;
+nonfix ++ -- RL mem;
val explode = String.explode;
val implode = String.implode;
val print = TextIO.print;
@@ -12157,7 +12157,7 @@
structure Metis = struct open Metis
(* Metis-specific ML environment *)
-nonfix ++ -- RL mem union subset;
+nonfix ++ -- RL mem;
val explode = String.explode;
val implode = String.implode;
val print = TextIO.print;
@@ -12408,7 +12408,7 @@
structure Metis = struct open Metis
(* Metis-specific ML environment *)
-nonfix ++ -- RL mem union subset;
+nonfix ++ -- RL mem;
val explode = String.explode;
val implode = String.implode;
val print = TextIO.print;
@@ -12890,7 +12890,7 @@
structure Metis = struct open Metis
(* Metis-specific ML environment *)
-nonfix ++ -- RL mem union subset;
+nonfix ++ -- RL mem;
val explode = String.explode;
val implode = String.implode;
val print = TextIO.print;
@@ -13015,7 +13015,7 @@
structure Metis = struct open Metis
(* Metis-specific ML environment *)
-nonfix ++ -- RL mem union subset;
+nonfix ++ -- RL mem;
val explode = String.explode;
val implode = String.implode;
val print = TextIO.print;
@@ -13156,7 +13156,7 @@
structure Metis = struct open Metis
(* Metis-specific ML environment *)
-nonfix ++ -- RL mem union subset;
+nonfix ++ -- RL mem;
val explode = String.explode;
val implode = String.implode;
val print = TextIO.print;
@@ -13528,7 +13528,7 @@
structure Metis = struct open Metis
(* Metis-specific ML environment *)
-nonfix ++ -- RL mem union subset;
+nonfix ++ -- RL mem;
val explode = String.explode;
val implode = String.implode;
val print = TextIO.print;
@@ -13882,7 +13882,7 @@
structure Metis = struct open Metis
(* Metis-specific ML environment *)
-nonfix ++ -- RL mem union subset;
+nonfix ++ -- RL mem;
val explode = String.explode;
val implode = String.implode;
val print = TextIO.print;
@@ -14599,7 +14599,7 @@
structure Metis = struct open Metis
(* Metis-specific ML environment *)
-nonfix ++ -- RL mem union subset;
+nonfix ++ -- RL mem;
val explode = String.explode;
val implode = String.implode;
val print = TextIO.print;
@@ -14826,7 +14826,7 @@
structure Metis = struct open Metis
(* Metis-specific ML environment *)
-nonfix ++ -- RL mem union subset;
+nonfix ++ -- RL mem;
val explode = String.explode;
val implode = String.implode;
val print = TextIO.print;
@@ -15243,7 +15243,7 @@
structure Metis = struct open Metis
(* Metis-specific ML environment *)
-nonfix ++ -- RL mem union subset;
+nonfix ++ -- RL mem;
val explode = String.explode;
val implode = String.implode;
val print = TextIO.print;
@@ -16110,7 +16110,7 @@
structure Metis = struct open Metis
(* Metis-specific ML environment *)
-nonfix ++ -- RL mem union subset;
+nonfix ++ -- RL mem;
val explode = String.explode;
val implode = String.implode;
val print = TextIO.print;
@@ -16362,7 +16362,7 @@
structure Metis = struct open Metis
(* Metis-specific ML environment *)
-nonfix ++ -- RL mem union subset;
+nonfix ++ -- RL mem;
val explode = String.explode;
val implode = String.implode;
val print = TextIO.print;
@@ -16563,7 +16563,7 @@
structure Metis = struct open Metis
(* Metis-specific ML environment *)
-nonfix ++ -- RL mem union subset;
+nonfix ++ -- RL mem;
val explode = String.explode;
val implode = String.implode;
val print = TextIO.print;
--- a/src/Tools/Metis/src/PortableIsabelle.sml Sun Nov 08 15:45:09 2009 +0100
+++ b/src/Tools/Metis/src/PortableIsabelle.sml Sun Nov 08 20:50:31 2009 +0100
@@ -33,10 +33,10 @@
(* Generating random values. *)
(* ------------------------------------------------------------------------- *)
-val randomWord = RandomWord.next_word;
-val randomBool = RandomWord.next_bool;
-fun randomInt n = RandomWord.next_int 0 (n - 1);
-val randomReal = RandomWord.next_real;
+val randomWord = Random_Word.next_word;
+val randomBool = Random_Word.next_bool;
+fun randomInt n = Random_Word.next_int 0 (n - 1);
+val randomReal = Random_Word.next_real;
end;
--- a/src/Tools/induct.ML Sun Nov 08 15:45:09 2009 +0100
+++ b/src/Tools/induct.ML Sun Nov 08 20:50:31 2009 +0100
@@ -130,7 +130,7 @@
(* context data *)
-structure InductData = GenericDataFun
+structure InductData = Generic_Data
(
type T = (rules * rules) * (rules * rules) * (rules * rules);
val empty =
@@ -138,7 +138,7 @@
(init_rules (right_var_concl o #2), init_rules (Thm.major_prem_of o #2)),
(init_rules (left_var_concl o #2), init_rules (Thm.concl_of o #2)));
val extend = I;
- fun merge _ (((casesT1, casesP1), (inductT1, inductP1), (coinductT1, coinductP1)),
+ fun merge (((casesT1, casesP1), (inductT1, inductP1), (coinductT1, coinductP1)),
((casesT2, casesP2), (inductT2, inductP2), (coinductT2, coinductP2))) =
((Item_Net.merge (casesT1, casesT2), Item_Net.merge (casesP1, casesP2)),
(Item_Net.merge (inductT1, inductT2), Item_Net.merge (inductP1, inductP2)),
--- a/src/Tools/nbe.ML Sun Nov 08 15:45:09 2009 +0100
+++ b/src/Tools/nbe.ML Sun Nov 08 20:50:31 2009 +0100
@@ -37,13 +37,12 @@
(** certificates and oracle for "trivial type classes" **)
-structure Triv_Class_Data = TheoryDataFun
+structure Triv_Class_Data = Theory_Data
(
type T = (class * thm) list;
val empty = [];
- val copy = I;
val extend = I;
- fun merge pp = AList.merge (op =) (K true);
+ fun merge data : T = AList.merge (op =) (K true) data;
);
fun add_const_alias thm thy =
--- a/src/Tools/quickcheck.ML Sun Nov 08 15:45:09 2009 +0100
+++ b/src/Tools/quickcheck.ML Sun Nov 08 20:50:31 2009 +0100
@@ -52,16 +52,16 @@
make_test_params ((Int.max (size1, size2), Int.max (iterations1, iterations2)),
case default_type1 of NONE => default_type2 | _ => default_type1);
-structure Data = TheoryDataFun(
+structure Data = Theory_Data
+(
type T = (string * (Proof.context -> term -> int -> term list option)) list
* test_params;
val empty = ([], Test_Params { size = 10, iterations = 100, default_type = NONE });
- val copy = I;
val extend = I;
- fun merge pp ((generators1, params1), (generators2, params2)) =
- (AList.merge (op = : string * string -> bool) (K true) (generators1, generators2),
+ fun merge ((generators1, params1), (generators2, params2)) : T =
+ (AList.merge (op =) (K true) (generators1, generators2),
merge_test_params (params1, params2));
-)
+);
val add_generator = Data.map o apfst o AList.update (op =);
--- a/src/Tools/random_word.ML Sun Nov 08 15:45:09 2009 +0100
+++ b/src/Tools/random_word.ML Sun Nov 08 20:50:31 2009 +0100
@@ -18,7 +18,7 @@
val pick_weighted: (int * 'a) list -> 'a
end;
-structure RandomWord: RANDOM_WORD =
+structure Random_Word: RANDOM_WORD =
struct
(* random words: 0w0 <= result <= max_word *)
--- a/src/Tools/value.ML Sun Nov 08 15:45:09 2009 +0100
+++ b/src/Tools/value.ML Sun Nov 08 20:50:31 2009 +0100
@@ -15,12 +15,12 @@
structure Value : VALUE =
struct
-structure Evaluator = TheoryDataFun(
+structure Evaluator = Theory_Data
+(
type T = (string * (Proof.context -> term -> term)) list;
val empty = [];
- val copy = I;
val extend = I;
- fun merge _ data = AList.merge (op =) (K true) data;
+ fun merge data : T = AList.merge (op =) (K true) data;
)
val add_evaluator = Evaluator.map o AList.update (op =);
--- a/src/ZF/Tools/ind_cases.ML Sun Nov 08 15:45:09 2009 +0100
+++ b/src/ZF/Tools/ind_cases.ML Sun Nov 08 20:50:31 2009 +0100
@@ -18,13 +18,12 @@
(* theory data *)
-structure IndCasesData = TheoryDataFun
+structure IndCasesData = Theory_Data
(
type T = (simpset -> cterm -> thm) Symtab.table;
val empty = Symtab.empty;
- val copy = I;
val extend = I;
- fun merge _ tabs : T = Symtab.merge (K true) tabs;
+ fun merge data = Symtab.merge (K true) data;
);
--- a/src/ZF/Tools/induct_tacs.ML Sun Nov 08 15:45:09 2009 +0100
+++ b/src/ZF/Tools/induct_tacs.ML Sun Nov 08 20:50:31 2009 +0100
@@ -29,13 +29,12 @@
mutual_induct : thm,
exhaustion : thm};
-structure DatatypesData = TheoryDataFun
+structure DatatypesData = Theory_Data
(
type T = datatype_info Symtab.table;
val empty = Symtab.empty;
- val copy = I;
val extend = I;
- fun merge _ tabs : T = Symtab.merge (K true) tabs;
+ fun merge data : T = Symtab.merge (K true) data;
);
@@ -49,13 +48,12 @@
rec_rewrites : thm list}; (*recursor equations*)
-structure ConstructorsData = TheoryDataFun
+structure ConstructorsData = Theory_Data
(
type T = constructor_info Symtab.table
val empty = Symtab.empty
- val copy = I;
val extend = I
- fun merge _ tabs : T = Symtab.merge (K true) tabs;
+ fun merge data = Symtab.merge (K true) data;
);
structure DatatypeTactics : DATATYPE_TACTICS =
--- a/src/ZF/Tools/typechk.ML Sun Nov 08 15:45:09 2009 +0100
+++ b/src/ZF/Tools/typechk.ML Sun Nov 08 20:50:31 2009 +0100
@@ -43,15 +43,13 @@
(* generic data *)
-structure Data = GenericDataFun
+structure Data = Generic_Data
(
- type T = tcset
+ type T = tcset;
val empty = TC {rules = [], net = Net.empty};
val extend = I;
-
- fun merge _ (TC {rules, net}, TC {rules = rules', net = net'}) =
- TC {rules = Thm.merge_thms (rules, rules'),
- net = Net.merge Thm.eq_thm_prop (net, net')};
+ fun merge (TC {rules, net}, TC {rules = rules', net = net'}) =
+ TC {rules = Thm.merge_thms (rules, rules'), net = Net.merge Thm.eq_thm_prop (net, net')};
);
val TC_add = Thm.declaration_attribute (Data.map o add_rule);