misc tuning and comments based on review of Theory_Data, Proof_Data, Generic_Data usage;
authorwenzelm
Sat Jan 08 17:14:48 2011 +0100 (2011-01-08)
changeset 41472f6ab14e61604
parent 41471 54a58904a598
child 41473 3717fc42ebe9
misc tuning and comments based on review of Theory_Data, Proof_Data, Generic_Data usage;
src/HOL/Boogie/Tools/boogie_vcs.ML
src/HOL/Library/Eval_Witness.thy
src/HOL/Mirabelle/Tools/mirabelle.ML
src/HOL/Statespace/state_fun.ML
src/HOL/Statespace/state_space.ML
src/HOL/Tools/Function/partial_function.ML
src/HOL/Tools/Nitpick/nitpick_hol.ML
src/HOL/Tools/Nitpick/nitpick_isar.ML
src/HOL/Tools/Nitpick/nitpick_model.ML
src/HOL/Tools/Predicate_Compile/code_prolog.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML
src/HOL/Tools/Qelim/cooper.ML
src/HOL/Tools/Quotient/quotient_info.ML
src/HOL/Tools/SMT/smt_config.ML
src/HOL/Tools/SMT/smt_solver.ML
src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
src/HOL/Tools/code_evaluation.ML
src/HOL/Tools/inductive_codegen.ML
src/HOL/Tools/inductive_set.ML
src/HOL/Tools/quickcheck_generators.ML
src/HOL/Tools/refute.ML
src/HOL/Tools/smallvalue_generators.ML
src/HOL/Tools/type_lifting.ML
src/Pure/Isar/code.ML
src/Pure/Isar/spec_rules.ML
src/Pure/Isar/specification.ML
src/Tools/Code/code_runtime.ML
src/Tools/adhoc_overloading.ML
src/Tools/nbe.ML
src/Tools/quickcheck.ML
     1.1 --- a/src/HOL/Boogie/Tools/boogie_vcs.ML	Sat Jan 08 16:01:51 2011 +0100
     1.2 +++ b/src/HOL/Boogie/Tools/boogie_vcs.ML	Sat Jan 08 17:14:48 2011 +0100
     1.3 @@ -254,7 +254,7 @@
     1.4  end
     1.5  
     1.6  
     1.7 -(* the VC store *)
     1.8 +(* the VC store *)  (* FIXME just one data slot (record) per program unit *)
     1.9  
    1.10  fun err_unfinished () = error "An unfinished Boogie environment is still open."
    1.11  
     2.1 --- a/src/HOL/Library/Eval_Witness.thy	Sat Jan 08 16:01:51 2011 +0100
     2.2 +++ b/src/HOL/Library/Eval_Witness.thy	Sat Jan 08 17:14:48 2011 +0100
     2.3 @@ -45,8 +45,10 @@
     2.4  instance list :: (ml_equiv) ml_equiv ..
     2.5  
     2.6  ML {*
     2.7 -structure Eval_Method = Proof_Data (
     2.8 +structure Eval_Method = Proof_Data
     2.9 +(
    2.10    type T = unit -> bool
    2.11 +  (* FIXME avoid user error with non-user text *)
    2.12    fun init _ () = error "Eval_Method"
    2.13  )
    2.14  *}
     3.1 --- a/src/HOL/Mirabelle/Tools/mirabelle.ML	Sat Jan 08 16:01:51 2011 +0100
     3.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle.ML	Sat Jan 08 17:14:48 2011 +0100
     3.3 @@ -66,7 +66,7 @@
     3.4    type T = (int * run_action * done_action) list
     3.5    val empty = []
     3.6    val extend = I
     3.7 -  fun merge data = Library.merge (K true) data  (* FIXME ?!? *)
     3.8 +  fun merge data = Library.merge (K true) data  (* FIXME exponential blowup because of (K true) *)
     3.9  )
    3.10  
    3.11  
     4.1 --- a/src/HOL/Statespace/state_fun.ML	Sat Jan 08 16:01:51 2011 +0100
     4.2 +++ b/src/HOL/Statespace/state_fun.ML	Sat Jan 08 17:14:48 2011 +0100
     4.3 @@ -101,7 +101,7 @@
     4.4    val empty = (empty_ss, empty_ss, false);
     4.5    val extend = I;
     4.6    fun merge ((ss1, ex_ss1, b1), (ss2, ex_ss2, b2)) =
     4.7 -    (merge_ss (ss1, ss2), merge_ss (ex_ss1, ex_ss2), b1 orelse b2);
     4.8 +    (merge_ss (ss1, ss2), merge_ss (ex_ss1, ex_ss2), b1 orelse b2 (* FIXME odd merge *));
     4.9  );
    4.10  
    4.11  val init_state_fun_data =
     5.1 --- a/src/HOL/Statespace/state_space.ML	Sat Jan 08 16:01:51 2011 +0100
     5.2 +++ b/src/HOL/Statespace/state_space.ML	Sat Jan 08 17:14:48 2011 +0100
     5.3 @@ -115,7 +115,7 @@
     5.4        {declinfo=declinfo2, distinctthm=distinctthm2, silent=silent2}) : T =
     5.5      {declinfo = Termtab.merge (K true) (declinfo1, declinfo2),
     5.6       distinctthm = Symtab.merge (K true) (distinctthm1, distinctthm2),
     5.7 -     silent = silent1 andalso silent2}
     5.8 +     silent = silent1 andalso silent2 (* FIXME odd merge *)}
     5.9  );
    5.10  
    5.11  fun make_namespace_data declinfo distinctthm silent =
     6.1 --- a/src/HOL/Tools/Function/partial_function.ML	Sat Jan 08 16:01:51 2011 +0100
     6.2 +++ b/src/HOL/Tools/Function/partial_function.ML	Sat Jan 08 17:14:48 2011 +0100
     6.3 @@ -27,7 +27,7 @@
     6.4    type T = ((term * term) * thm) Symtab.table;
     6.5    val empty = Symtab.empty;
     6.6    val extend = I;
     6.7 -  fun merge (a, b) = Symtab.merge (K true) (a, b);
     6.8 +  fun merge data = Symtab.merge (K true) data;
     6.9  )
    6.10  
    6.11  fun init fixp mono fixp_eq phi =
     7.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Sat Jan 08 16:01:51 2011 +0100
     7.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Sat Jan 08 17:14:48 2011 +0100
     7.3 @@ -275,7 +275,8 @@
     7.4  datatype boxability =
     7.5    InConstr | InSel | InExpr | InPair | InFunLHS | InFunRHS1 | InFunRHS2
     7.6  
     7.7 -structure Data = Generic_Data(
     7.8 +structure Data = Generic_Data
     7.9 +(
    7.10    type T = {frac_types: (string * (string * string) list) list,
    7.11              codatatypes: (string * (string * styp list)) list}
    7.12    val empty = {frac_types = [], codatatypes = []}
    7.13 @@ -283,7 +284,8 @@
    7.14    fun merge ({frac_types = fs1, codatatypes = cs1},
    7.15               {frac_types = fs2, codatatypes = cs2}) : T =
    7.16      {frac_types = AList.merge (op =) (K true) (fs1, fs2),
    7.17 -     codatatypes = AList.merge (op =) (K true) (cs1, cs2)})
    7.18 +     codatatypes = AList.merge (op =) (K true) (cs1, cs2)}
    7.19 +)
    7.20  
    7.21  val name_sep = "$"
    7.22  val numeral_prefix = nitpick_prefix ^ "num" ^ name_sep
     8.1 --- a/src/HOL/Tools/Nitpick/nitpick_isar.ML	Sat Jan 08 16:01:51 2011 +0100
     8.2 +++ b/src/HOL/Tools/Nitpick/nitpick_isar.ML	Sat Jan 08 17:14:48 2011 +0100
     8.3 @@ -130,11 +130,13 @@
     8.4              else
     8.5                [(name, value)]
     8.6  
     8.7 -structure Data = Theory_Data(
     8.8 +structure Data = Theory_Data
     8.9 +(
    8.10    type T = raw_param list
    8.11    val empty = map (apsnd single) default_default_params
    8.12    val extend = I
    8.13 -  fun merge (x, y) = AList.merge (op =) (K true) (x, y))
    8.14 +  fun merge data = AList.merge (op =) (K true) data
    8.15 +)
    8.16  
    8.17  val set_default_raw_param =
    8.18    Data.map o fold (AList.update (op =)) o normalize_raw_param
     9.1 --- a/src/HOL/Tools/Nitpick/nitpick_model.ML	Sat Jan 08 16:01:51 2011 +0100
     9.2 +++ b/src/HOL/Tools/Nitpick/nitpick_model.ML	Sat Jan 08 17:14:48 2011 +0100
     9.3 @@ -63,11 +63,13 @@
     9.4  type term_postprocessor =
     9.5    Proof.context -> string -> (typ -> term list) -> typ -> term -> term
     9.6  
     9.7 -structure Data = Generic_Data(
     9.8 +structure Data = Generic_Data
     9.9 +(
    9.10    type T = (typ * term_postprocessor) list
    9.11    val empty = []
    9.12    val extend = I
    9.13 -  fun merge (x, y) = AList.merge (op =) (K true) (x, y))
    9.14 +  fun merge data = AList.merge (op =) (K true) data
    9.15 +)
    9.16  
    9.17  fun xsym s s' () = if print_mode_active Symbol.xsymbolsN then s else s'
    9.18  
    10.1 --- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Sat Jan 08 16:01:51 2011 +0100
    10.2 +++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Sat Jan 08 17:14:48 2011 +0100
    10.3 @@ -81,7 +81,7 @@
    10.4  fun merge_global_limit (NONE, NONE) = NONE
    10.5    | merge_global_limit (NONE, SOME n) = SOME n
    10.6    | merge_global_limit (SOME n, NONE) = SOME n
    10.7 -  | merge_global_limit (SOME n, SOME m) = SOME (Int.max (n, m))
    10.8 +  | merge_global_limit (SOME n, SOME m) = SOME (Int.max (n, m))  (* FIXME odd merge *)
    10.9     
   10.10  structure Options = Theory_Data
   10.11  (
   10.12 @@ -96,7 +96,7 @@
   10.13       {ensure_groundness = ensure_groundness2, limit_globally = limit_globally2,
   10.14        limited_types = limited_types2, limited_predicates = limited_predicates2,
   10.15        replacing = replacing2, manual_reorder = manual_reorder2}) =
   10.16 -    {ensure_groundness = ensure_groundness1 orelse ensure_groundness2,
   10.17 +    {ensure_groundness = ensure_groundness1 orelse ensure_groundness2 (* FIXME odd merge *),
   10.18       limit_globally = merge_global_limit (limit_globally1, limit_globally2),
   10.19       limited_types = AList.merge (op =) (K true) (limited_types1, limited_types2),
   10.20       limited_predicates = AList.merge (op =) (K true) (limited_predicates1, limited_predicates2),
   10.21 @@ -122,9 +122,7 @@
   10.22    type T = system_configuration
   10.23    val empty = {timeout = seconds 10.0, prolog_system = SWI_PROLOG}
   10.24    val extend = I;
   10.25 -  fun merge ({timeout = timeout1, prolog_system = prolog_system1},
   10.26 -        {timeout = timeout2, prolog_system = prolog_system2}) =
   10.27 -    {timeout = timeout1, prolog_system = prolog_system1}
   10.28 +  fun merge (a, _) = a
   10.29  )
   10.30  
   10.31  (* general string functions *)
    11.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Sat Jan 08 16:01:51 2011 +0100
    11.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Sat Jan 08 17:14:48 2011 +0100
    11.3 @@ -1625,44 +1625,60 @@
    11.4  
    11.5  (* transformation for code generation *)
    11.6  
    11.7 -structure Pred_Result = Proof_Data (
    11.8 +(* FIXME just one data slot (record) per program unit *)
    11.9 +
   11.10 +structure Pred_Result = Proof_Data
   11.11 +(
   11.12    type T = unit -> term Predicate.pred
   11.13 +  (* FIXME avoid user error with non-user text *)
   11.14    fun init _ () = error "Pred_Result"
   11.15  );
   11.16  val put_pred_result = Pred_Result.put;
   11.17  
   11.18 -structure Pred_Random_Result = Proof_Data (
   11.19 +structure Pred_Random_Result = Proof_Data
   11.20 +(
   11.21    type T = unit -> int * int -> term Predicate.pred * (int * int)
   11.22 +  (* FIXME avoid user error with non-user text *)
   11.23    fun init _ () = error "Pred_Random_Result"
   11.24  );
   11.25  val put_pred_random_result = Pred_Random_Result.put;
   11.26  
   11.27 -structure Dseq_Result = Proof_Data (
   11.28 +structure Dseq_Result = Proof_Data
   11.29 +(
   11.30    type T = unit -> term DSequence.dseq
   11.31 +  (* FIXME avoid user error with non-user text *)
   11.32    fun init _ () = error "Dseq_Result"
   11.33  );
   11.34  val put_dseq_result = Dseq_Result.put;
   11.35  
   11.36 -structure Dseq_Random_Result = Proof_Data (
   11.37 +structure Dseq_Random_Result = Proof_Data
   11.38 +(
   11.39    type T = unit -> int -> int -> int * int -> term DSequence.dseq * (int * int)
   11.40 +  (* FIXME avoid user error with non-user text *)
   11.41    fun init _ () = error "Dseq_Random_Result"
   11.42  );
   11.43  val put_dseq_random_result = Dseq_Random_Result.put;
   11.44  
   11.45 -structure New_Dseq_Result = Proof_Data (
   11.46 +structure New_Dseq_Result = Proof_Data
   11.47 +(
   11.48    type T = unit -> int -> term Lazy_Sequence.lazy_sequence
   11.49 +  (* FIXME avoid user error with non-user text *)
   11.50    fun init _ () = error "New_Dseq_Random_Result"
   11.51  );
   11.52  val put_new_dseq_result = New_Dseq_Result.put;
   11.53  
   11.54 -structure Lseq_Random_Result = Proof_Data (
   11.55 +structure Lseq_Random_Result = Proof_Data
   11.56 +(
   11.57    type T = unit -> int -> int -> int * int -> int -> term Lazy_Sequence.lazy_sequence
   11.58 +  (* FIXME avoid user error with non-user text *)
   11.59    fun init _ () = error "Lseq_Random_Result"
   11.60  );
   11.61  val put_lseq_random_result = Lseq_Random_Result.put;
   11.62  
   11.63 -structure Lseq_Random_Stats_Result = Proof_Data (
   11.64 +structure Lseq_Random_Stats_Result = Proof_Data
   11.65 +(
   11.66    type T = unit -> int -> int -> int * int -> int -> (term * int) Lazy_Sequence.lazy_sequence
   11.67 +  (* FIXME avoid user error with non-user text *)
   11.68    fun init _ () = error "Lseq_Random_Stats_Result"
   11.69  );
   11.70  val put_lseq_random_stats_result = Lseq_Random_Stats_Result.put;
    12.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML	Sat Jan 08 16:01:51 2011 +0100
    12.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML	Sat Jan 08 17:14:48 2011 +0100
    12.3 @@ -35,26 +35,36 @@
    12.4  
    12.5  open Predicate_Compile_Aux;
    12.6  
    12.7 -structure Pred_Result = Proof_Data (
    12.8 +(* FIXME just one data slot (record) per program unit *)
    12.9 +
   12.10 +structure Pred_Result = Proof_Data
   12.11 +(
   12.12    type T = unit -> int -> int -> int -> int * int -> term list Predicate.pred
   12.13 +  (* FIXME avoid user error with non-user text *)
   12.14    fun init _ () = error "Pred_Result"
   12.15  );
   12.16  val put_pred_result = Pred_Result.put;
   12.17  
   12.18 -structure Dseq_Result = Proof_Data (
   12.19 +structure Dseq_Result = Proof_Data
   12.20 +(
   12.21    type T = unit -> int -> int -> int * int -> term list DSequence.dseq * (int * int)
   12.22 +  (* FIXME avoid user error with non-user text *)
   12.23    fun init _ () = error "Dseq_Result"
   12.24  );
   12.25  val put_dseq_result = Dseq_Result.put;
   12.26  
   12.27 -structure Lseq_Result = Proof_Data (
   12.28 +structure Lseq_Result = Proof_Data
   12.29 +(
   12.30    type T = unit -> int -> int -> int * int -> int -> term list Lazy_Sequence.lazy_sequence
   12.31 +  (* FIXME avoid user error with non-user text *)
   12.32    fun init _ () = error "Lseq_Result"
   12.33  );
   12.34  val put_lseq_result = Lseq_Result.put;
   12.35  
   12.36 -structure New_Dseq_Result = Proof_Data (
   12.37 +structure New_Dseq_Result = Proof_Data
   12.38 +(
   12.39    type T = unit -> int -> term list Lazy_Sequence.lazy_sequence
   12.40 +  (* FIXME avoid user error with non-user text *)
   12.41    fun init _ () = error "New_Dseq_Random_Result"
   12.42  );
   12.43  val put_new_dseq_result = New_Dseq_Result.put;
    13.1 --- a/src/HOL/Tools/Qelim/cooper.ML	Sat Jan 08 16:01:51 2011 +0100
    13.2 +++ b/src/HOL/Tools/Qelim/cooper.ML	Sat Jan 08 17:14:48 2011 +0100
    13.3 @@ -51,7 +51,7 @@
    13.4  (
    13.5    type T = simpset * term list;
    13.6    val empty = (HOL_ss, allowed_consts);
    13.7 -  val extend  = I;
    13.8 +  val extend = I;
    13.9    fun merge ((ss1, ts1), (ss2, ts2)) =
   13.10      (merge_ss (ss1, ss2), Library.merge (op aconv) (ts1, ts2));
   13.11  );
    14.1 --- a/src/HOL/Tools/Quotient/quotient_info.ML	Sat Jan 08 16:01:51 2011 +0100
    14.2 +++ b/src/HOL/Tools/Quotient/quotient_info.ML	Sat Jan 08 17:14:48 2011 +0100
    14.3 @@ -55,6 +55,8 @@
    14.4  
    14.5  (** data containers **)
    14.6  
    14.7 +(* FIXME just one data slot (record) per program unit *)
    14.8 +
    14.9  (* info about map- and rel-functions for a type *)
   14.10  type maps_info = {mapfun: string, relmap: string}
   14.11  
    15.1 --- a/src/HOL/Tools/SMT/smt_config.ML	Sat Jan 08 16:01:51 2011 +0100
    15.2 +++ b/src/HOL/Tools/SMT/smt_config.ML	Sat Jan 08 17:14:48 2011 +0100
    15.3 @@ -68,7 +68,7 @@
    15.4    type T = (solver_info * string list) Symtab.table * string option
    15.5    val empty = (Symtab.empty, NONE)
    15.6    val extend = I
    15.7 -  fun merge ((ss1, s), (ss2, _)) = (Symtab.merge (K true) (ss1, ss2), s)
    15.8 +  fun merge ((ss1, s), (ss2, _)) = (Symtab.merge (K true) (ss1, ss2), s (* FIXME merge options!? *))
    15.9  )
   15.10  
   15.11  fun set_solver_options (name, options) =
   15.12 @@ -227,7 +227,7 @@
   15.13    type T = Cache_IO.cache option
   15.14    val empty = NONE
   15.15    val extend = I
   15.16 -  fun merge (s, _) = s
   15.17 +  fun merge (s, _) = s  (* FIXME merge options!? *)
   15.18  )
   15.19  
   15.20  val get_certificates_path =
    16.1 --- a/src/HOL/Tools/SMT/smt_solver.ML	Sat Jan 08 16:01:51 2011 +0100
    16.2 +++ b/src/HOL/Tools/SMT/smt_solver.ML	Sat Jan 08 17:14:48 2011 +0100
    16.3 @@ -176,6 +176,7 @@
    16.4    val extend = I
    16.5    fun merge data = Symtab.merge (K true) data
    16.6      handle Symtab.DUP name => error ("Duplicate SMT solver: " ^ quote name)
    16.7 +    (* FIXME never happens because of (K true) *)
    16.8  )
    16.9  
   16.10  local
    17.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Sat Jan 08 16:01:51 2011 +0100
    17.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Sat Jan 08 17:14:48 2011 +0100
    17.3 @@ -133,11 +133,13 @@
    17.4                              | _ => value)
    17.5      | NONE => (name, value)
    17.6  
    17.7 -structure Data = Theory_Data(
    17.8 +structure Data = Theory_Data
    17.9 +(
   17.10    type T = raw_param list
   17.11    val empty = default_default_params |> map (apsnd single)
   17.12    val extend = I
   17.13 -  fun merge p : T = AList.merge (op =) (K true) p)
   17.14 +  fun merge data : T = AList.merge (op =) (K true) data
   17.15 +)
   17.16  
   17.17  fun remotify_prover_if_available_and_not_already_remote ctxt name =
   17.18    if String.isPrefix remote_prefix name then
    18.1 --- a/src/HOL/Tools/code_evaluation.ML	Sat Jan 08 16:01:51 2011 +0100
    18.2 +++ b/src/HOL/Tools/code_evaluation.ML	Sat Jan 08 17:14:48 2011 +0100
    18.3 @@ -156,8 +156,10 @@
    18.4  
    18.5  (** evaluation **)
    18.6  
    18.7 -structure Evaluation = Proof_Data (
    18.8 +structure Evaluation = Proof_Data
    18.9 +(
   18.10    type T = unit -> term
   18.11 +  (* FIXME avoid user error with non-user text *)
   18.12    fun init _ () = error "Evaluation"
   18.13  );
   18.14  val put_term = Evaluation.put;
    19.1 --- a/src/HOL/Tools/inductive_codegen.ML	Sat Jan 08 16:01:51 2011 +0100
    19.2 +++ b/src/HOL/Tools/inductive_codegen.ML	Sat Jan 08 17:14:48 2011 +0100
    19.3 @@ -31,8 +31,9 @@
    19.4    val empty =
    19.5      {intros = Symtab.empty, graph = Graph.empty, eqns = Symtab.empty};
    19.6    val extend = I;
    19.7 -  fun merge ({intros=intros1, graph=graph1, eqns=eqns1},
    19.8 -    {intros=intros2, graph=graph2, eqns=eqns2}) : T =
    19.9 +  fun merge
   19.10 +    ({intros = intros1, graph = graph1, eqns = eqns1},
   19.11 +      {intros = intros2, graph = graph2, eqns = eqns2}) : T =
   19.12      {intros = merge_rules (intros1, intros2),
   19.13       graph = Graph.merge (K true) (graph1, graph2),
   19.14       eqns = merge_rules (eqns1, eqns2)};
    20.1 --- a/src/HOL/Tools/inductive_set.ML	Sat Jan 08 16:01:51 2011 +0100
    20.2 +++ b/src/HOL/Tools/inductive_set.ML	Sat Jan 08 17:14:48 2011 +0100
    20.3 @@ -175,8 +175,8 @@
    20.4        set_arities = set_arities2, pred_arities = pred_arities2}) : T =
    20.5      {to_set_simps = Thm.merge_thms (to_set_simps1, to_set_simps2),
    20.6       to_pred_simps = Thm.merge_thms (to_pred_simps1, to_pred_simps2),
    20.7 -     set_arities = Symtab.merge_list op = (set_arities1, set_arities2),
    20.8 -     pred_arities = Symtab.merge_list op = (pred_arities1, pred_arities2)};
    20.9 +     set_arities = Symtab.merge_list (op =) (set_arities1, set_arities2),
   20.10 +     pred_arities = Symtab.merge_list (op =) (pred_arities1, pred_arities2)};
   20.11  );
   20.12  
   20.13  fun name_type_of (Free p) = SOME p
    21.1 --- a/src/HOL/Tools/quickcheck_generators.ML	Sat Jan 08 16:01:51 2011 +0100
    21.2 +++ b/src/HOL/Tools/quickcheck_generators.ML	Sat Jan 08 17:14:48 2011 +0100
    21.3 @@ -307,14 +307,20 @@
    21.4  
    21.5  (** building and compiling generator expressions **)
    21.6  
    21.7 -structure Counterexample = Proof_Data (
    21.8 +(* FIXME just one data slot (record) per program unit *)
    21.9 +
   21.10 +structure Counterexample = Proof_Data
   21.11 +(
   21.12    type T = unit -> int -> int * int -> term list option * (int * int)
   21.13 +  (* FIXME avoid user error with non-user text *)
   21.14    fun init _ () = error "Counterexample"
   21.15  );
   21.16  val put_counterexample = Counterexample.put;
   21.17  
   21.18 -structure Counterexample_Report = Proof_Data (
   21.19 +structure Counterexample_Report = Proof_Data
   21.20 +(
   21.21    type T = unit -> int -> seed -> (term list option * (bool list * bool)) * seed
   21.22 +  (* FIXME avoid user error with non-user text *)
   21.23    fun init _ () = error "Counterexample_Report"
   21.24  );
   21.25  val put_counterexample_report = Counterexample_Report.put;
    22.1 --- a/src/HOL/Tools/refute.ML	Sat Jan 08 16:01:51 2011 +0100
    22.2 +++ b/src/HOL/Tools/refute.ML	Sat Jan 08 17:14:48 2011 +0100
    22.3 @@ -221,7 +221,7 @@
    22.4       {interpreters = in2, printers = pr2, parameters = pa2}) : T =
    22.5      {interpreters = AList.merge (op =) (K true) (in1, in2),
    22.6       printers = AList.merge (op =) (K true) (pr1, pr2),
    22.7 -     parameters = Symtab.merge (op=) (pa1, pa2)};
    22.8 +     parameters = Symtab.merge (op =) (pa1, pa2)};
    22.9  );
   22.10  
   22.11  val get_data = Data.get o ProofContext.theory_of;
    23.1 --- a/src/HOL/Tools/smallvalue_generators.ML	Sat Jan 08 16:01:51 2011 +0100
    23.2 +++ b/src/HOL/Tools/smallvalue_generators.ML	Sat Jan 08 17:14:48 2011 +0100
    23.3 @@ -210,8 +210,10 @@
    23.4  
    23.5  (** building and compiling generator expressions **)
    23.6  
    23.7 -structure Counterexample = Proof_Data (
    23.8 +structure Counterexample = Proof_Data
    23.9 +(
   23.10    type T = unit -> int -> term list option
   23.11 +  (* FIXME avoid user error with non-user text *)
   23.12    fun init _ () = error "Counterexample"
   23.13  );
   23.14  val put_counterexample = Counterexample.put;
    24.1 --- a/src/HOL/Tools/type_lifting.ML	Sat Jan 08 16:01:51 2011 +0100
    24.2 +++ b/src/HOL/Tools/type_lifting.ML	Sat Jan 08 17:14:48 2011 +0100
    24.3 @@ -27,11 +27,12 @@
    24.4  type entry = { mapper: term, variances: (sort * (bool * bool)) list,
    24.5    comp: thm, id: thm };
    24.6  
    24.7 -structure Data = Generic_Data(
    24.8 +structure Data = Generic_Data
    24.9 +(
   24.10    type T = entry list Symtab.table
   24.11    val empty = Symtab.empty
   24.12 -  fun merge (xy : T * T) = Symtab.merge (K true) xy
   24.13    val extend = I
   24.14 +  fun merge data = Symtab.merge (K true) data
   24.15  );
   24.16  
   24.17  val entries = Data.get o Context.Proof;
    25.1 --- a/src/Pure/Isar/code.ML	Sat Jan 08 16:01:51 2011 +0100
    25.2 +++ b/src/Pure/Isar/code.ML	Sat Jan 08 17:14:48 2011 +0100
    25.3 @@ -263,7 +263,7 @@
    25.4    type T = spec * (data * theory_ref) option Synchronized.var;
    25.5    val empty = (make_spec (false, (((Symtab.empty, Symtab.empty), Symtab.empty),
    25.6      (Symtab.empty, (Symtab.empty, Symtab.empty)))), empty_dataref ());
    25.7 -  val extend = I
    25.8 +  val extend = I  (* FIXME empty_dataref!?! *)
    25.9    fun merge ((spec1, _), (spec2, _)) =
   25.10      (merge_spec (spec1, spec2), empty_dataref ());
   25.11  );
   25.12 @@ -1238,7 +1238,7 @@
   25.13  
   25.14  (** infrastructure **)
   25.15  
   25.16 -(* c.f. src/HOL/Tools/recfun_codegen.ML *)
   25.17 +(* cf. src/HOL/Tools/recfun_codegen.ML *)
   25.18  
   25.19  structure Code_Target_Attr = Theory_Data
   25.20  (
    26.1 --- a/src/Pure/Isar/spec_rules.ML	Sat Jan 08 16:01:51 2011 +0100
    26.2 +++ b/src/Pure/Isar/spec_rules.ML	Sat Jan 08 17:14:48 2011 +0100
    26.3 @@ -37,7 +37,7 @@
    26.4          eq_list Thm.eq_thm_prop (ths1, ths2))
    26.5        (#1 o #2);
    26.6    val extend = I;
    26.7 -  fun merge data = Item_Net.merge data;
    26.8 +  val merge = Item_Net.merge;
    26.9  );
   26.10  
   26.11  val get = Item_Net.content o Rules.get o Context.Proof;
    27.1 --- a/src/Pure/Isar/specification.ML	Sat Jan 08 16:01:51 2011 +0100
    27.2 +++ b/src/Pure/Isar/specification.ML	Sat Jan 08 17:14:48 2011 +0100
    27.3 @@ -366,7 +366,7 @@
    27.4    type T = ((bool -> Proof.state -> Proof.state) * stamp) list;
    27.5    val empty = [];
    27.6    val extend = I;
    27.7 -  fun merge hooks : T = Library.merge (eq_snd op =) hooks;
    27.8 +  fun merge data : T = Library.merge (eq_snd op =) data;
    27.9  );
   27.10  
   27.11  fun gen_theorem schematic prep_att prep_stmt
    28.1 --- a/src/Tools/Code/code_runtime.ML	Sat Jan 08 16:01:51 2011 +0100
    28.2 +++ b/src/Tools/Code/code_runtime.ML	Sat Jan 08 17:14:48 2011 +0100
    28.3 @@ -138,6 +138,7 @@
    28.4  structure Truth_Result = Proof_Data
    28.5  (
    28.6    type T = unit -> truth
    28.7 +  (* FIXME avoid user error with non-user text *)
    28.8    fun init _ () = error "Truth_Result"
    28.9  );
   28.10  val put_truth = Truth_Result.put;
   28.11 @@ -369,8 +370,8 @@
   28.12  (
   28.13    type T = string list
   28.14    val empty = []
   28.15 +  val extend = I
   28.16    fun merge data : T = Library.merge (op =) data
   28.17 -  val extend = I
   28.18  );
   28.19  
   28.20  fun notify_val (string, value) = 
    29.1 --- a/src/Tools/adhoc_overloading.ML	Sat Jan 08 16:01:51 2011 +0100
    29.2 +++ b/src/Tools/adhoc_overloading.ML	Sat Jan 08 17:14:48 2011 +0100
    29.3 @@ -53,10 +53,11 @@
    29.4      if ext_name1 = ext_name2 then ext_name1
    29.5      else duplicate_variant_err int_name ext_name1;
    29.6  
    29.7 -  fun merge ({internalize=int1, externalize=ext1},
    29.8 -      {internalize=int2, externalize=ext2}) =
    29.9 -    {internalize=Symtab.join (K (Library.merge (op =))) (int1, int2),
   29.10 -     externalize=Symtab.join merge_ext (ext1, ext2)};
   29.11 +  fun merge
   29.12 +    ({internalize = int1, externalize = ext1},
   29.13 +      {internalize = int2, externalize = ext2}) : T =
   29.14 +    {internalize = Symtab.join (K (Library.merge (op =))) (int1, int2),
   29.15 +      externalize = Symtab.join merge_ext (ext1, ext2)};
   29.16  );
   29.17  
   29.18  fun map_tables f g =
    30.1 --- a/src/Tools/nbe.ML	Sat Jan 08 16:01:51 2011 +0100
    30.2 +++ b/src/Tools/nbe.ML	Sat Jan 08 17:14:48 2011 +0100
    30.3 @@ -229,8 +229,10 @@
    30.4  
    30.5  (* nbe specific syntax and sandbox communication *)
    30.6  
    30.7 -structure Univs = Proof_Data (
    30.8 +structure Univs = Proof_Data
    30.9 +(
   30.10    type T = unit -> Univ list -> Univ list
   30.11 +  (* FIXME avoid user error with non-user text *)
   30.12    fun init _ () = error "Univs"
   30.13  );
   30.14  val put_result = Univs.put;
    31.1 --- a/src/Tools/quickcheck.ML	Sat Jan 08 16:01:51 2011 +0100
    31.2 +++ b/src/Tools/quickcheck.ML	Sat Jan 08 17:14:48 2011 +0100
    31.3 @@ -93,9 +93,10 @@
    31.4  fun map_test_params' f (Test_Params {default_type, expect}) = make_test_params (f (default_type, expect));
    31.5  
    31.6  fun merge_test_params
    31.7 - (Test_Params {default_type = default_type1, expect = expect1},
    31.8 -  Test_Params {default_type = default_type2, expect = expect2}) =
    31.9 -  make_test_params (merge (op =) (default_type1, default_type2), merge_expectation (expect1, expect2));
   31.10 +  (Test_Params {default_type = default_type1, expect = expect1},
   31.11 +    Test_Params {default_type = default_type2, expect = expect2}) =
   31.12 +  make_test_params
   31.13 +    (merge (op =) (default_type1, default_type2), merge_expectation (expect1, expect2));
   31.14  
   31.15  structure Data = Generic_Data
   31.16  (