simplified DataFun interfaces;
authorwenzelm
Mon May 07 00:49:59 2007 +0200 (2007-05-07)
changeset 22846fb79144af9a3
parent 22845 5f9138bcb3d7
child 22847 22da6c4bc422
simplified DataFun interfaces;
src/CCL/Wfd.thy
src/HOL/Algebra/ringsimp.ML
src/HOL/Hyperreal/transfer.ML
src/HOL/Import/hol4rews.ML
src/HOL/Import/import_package.ML
src/HOL/Import/shuffler.ML
src/HOL/Inductive.thy
src/HOL/Nominal/Nominal.thy
src/HOL/Nominal/nominal_atoms.ML
src/HOL/Nominal/nominal_package.ML
src/HOL/Nominal/nominal_thmdecls.ML
src/HOL/Predicate.thy
src/HOL/Tools/datatype_hooks.ML
src/HOL/Tools/datatype_package.ML
src/HOL/Tools/function_package/fundef_common.ML
src/HOL/Tools/function_package/fundef_package.ML
src/HOL/Tools/inductive_codegen.ML
src/HOL/Tools/inductive_package.ML
src/HOL/Tools/old_inductive_package.ML
src/HOL/Tools/recdef_package.ML
src/HOL/Tools/recfun_codegen.ML
src/HOL/Tools/record_package.ML
src/HOL/Tools/refute.ML
src/HOL/Tools/res_atpset.ML
src/HOL/Tools/res_axioms.ML
src/HOL/Tools/typecopy_package.ML
src/HOL/Tools/typedef_package.ML
src/HOL/Typedef.thy
src/HOL/arith_data.ML
src/Provers/Arith/fast_lin_arith.ML
src/Provers/classical.ML
src/Pure/Isar/attrib.ML
src/Pure/Isar/calculation.ML
src/Pure/Isar/context_rules.ML
src/Pure/Isar/induct_attrib.ML
src/Pure/Isar/local_defs.ML
src/Pure/Isar/local_theory.ML
src/Pure/Isar/locale.ML
src/Pure/Isar/method.ML
src/Pure/Isar/object_logic.ML
src/Pure/Isar/proof_context.ML
src/Pure/Isar/theory_target.ML
src/Pure/Proof/extraction.ML
src/Pure/Thy/present.ML
src/Pure/Thy/term_style.ML
src/Pure/Tools/class_package.ML
src/Pure/Tools/codegen_data.ML
src/Pure/Tools/codegen_names.ML
src/Pure/Tools/codegen_package.ML
src/Pure/Tools/codegen_serializer.ML
src/Pure/Tools/nbe.ML
src/Pure/assumption.ML
src/Pure/axclass.ML
src/Pure/codegen.ML
src/Pure/compress.ML
src/Pure/display.ML
src/Pure/proofterm.ML
src/Pure/pure_thy.ML
src/Pure/sign.ML
src/Pure/simplifier.ML
src/Pure/theory.ML
src/Pure/variable.ML
src/ZF/Tools/ind_cases.ML
src/ZF/Tools/induct_tacs.ML
src/ZF/Tools/typechk.ML
     1.1 --- a/src/CCL/Wfd.thy	Sun May 06 21:50:17 2007 +0200
     1.2 +++ b/src/CCL/Wfd.thy	Mon May 07 00:49:59 2007 +0200
     1.3 @@ -500,12 +500,10 @@
     1.4  
     1.5  structure Data = GenericDataFun
     1.6  (
     1.7 -  val name = "CCL/eval";
     1.8    type T = thm list;
     1.9    val empty = [];
    1.10    val extend = I;
    1.11    fun merge _ = Drule.merge_rules;
    1.12 -  fun print _ _ = ();
    1.13  );
    1.14  
    1.15  in
    1.16 @@ -518,7 +516,6 @@
    1.17      DEPTH_SOLVE_1 (resolve_tac (ths @ prems @ Data.get (Context.Proof ctxt)) 1)) 1;
    1.18  
    1.19  val eval_setup =
    1.20 -  Data.init #>
    1.21    Attrib.add_attributes
    1.22      [("eval", Attrib.add_del_args eval_add eval_del, "declaration of evaluation rule")] #>
    1.23    Method.add_methods [("eval", Method.thms_ctxt_args (fn ths => fn ctxt =>
     2.1 --- a/src/HOL/Algebra/ringsimp.ML	Sun May 06 21:50:17 2007 +0200
     2.2 +++ b/src/HOL/Algebra/ringsimp.ML	Mon May 07 00:49:59 2007 +0200
     2.3 @@ -20,9 +20,8 @@
     2.4  fun struct_eq ((s1: string, ts1), (s2, ts2)) =
     2.5    (s1 = s2) andalso eq_list (op aconv) (ts1, ts2);
     2.6  
     2.7 -structure AlgebraData = GenericDataFun
     2.8 -(struct
     2.9 -  val name = "Algebra/algebra";
    2.10 +structure Data = GenericDataFun
    2.11 +(
    2.12    type T = ((string * term list) * thm list) list;
    2.13      (* Algebraic structures:
    2.14         identifier of the structure, list of operations and simp rules,
    2.15 @@ -30,20 +29,16 @@
    2.16    val empty = [];
    2.17    val extend = I;
    2.18    fun merge _ = AList.join struct_eq (K (Library.merge Thm.eq_thm_prop));
    2.19 -  fun print generic structs =
    2.20 -    let
    2.21 -      val ctxt = Context.proof_of generic;
    2.22 -      val pretty_term = Pretty.quote o ProofContext.pretty_term ctxt;
    2.23 -      fun pretty_struct ((s, ts), _) = Pretty.block
    2.24 -        [Pretty.str s, Pretty.str ":", Pretty.brk 1,
    2.25 -         Pretty.enclose "(" ")" (Pretty.breaks (map pretty_term ts))];
    2.26 -    in
    2.27 -      Pretty.big_list "Algebraic structures:" (map pretty_struct structs) |>
    2.28 -        Pretty.writeln
    2.29 -    end
    2.30 -end);
    2.31 +);
    2.32  
    2.33 -val print_structures = AlgebraData.print o Context.Proof;
    2.34 +fun print_structures ctxt =
    2.35 +  let
    2.36 +    val structs = Data.get (Context.Proof ctxt);
    2.37 +    val pretty_term = Pretty.quote o ProofContext.pretty_term ctxt;
    2.38 +    fun pretty_struct ((s, ts), _) = Pretty.block
    2.39 +      [Pretty.str s, Pretty.str ":", Pretty.brk 1,
    2.40 +       Pretty.enclose "(" ")" (Pretty.breaks (map pretty_term ts))];
    2.41 +  in Pretty.writeln (Pretty.big_list "Algebraic structures:" (map pretty_struct structs)) end;
    2.42  
    2.43  
    2.44  (** Method **)
    2.45 @@ -57,17 +52,17 @@
    2.46    in asm_full_simp_tac (HOL_ss settermless less addsimps simps) end;
    2.47  
    2.48  fun algebra_tac ctxt =
    2.49 -  EVERY' (map (fn s => TRY o struct_tac s) (AlgebraData.get (Context.Proof ctxt)));
    2.50 +  EVERY' (map (fn s => TRY o struct_tac s) (Data.get (Context.Proof ctxt)));
    2.51  
    2.52  
    2.53  (** Attribute **)
    2.54  
    2.55  fun add_struct_thm s =
    2.56    Thm.declaration_attribute
    2.57 -    (fn thm => AlgebraData.map (AList.map_default struct_eq (s, []) (insert Thm.eq_thm_prop thm)));
    2.58 +    (fn thm => Data.map (AList.map_default struct_eq (s, []) (insert Thm.eq_thm_prop thm)));
    2.59  fun del_struct s =
    2.60    Thm.declaration_attribute
    2.61 -    (fn _ => AlgebraData.map (AList.delete struct_eq s));
    2.62 +    (fn _ => Data.map (AList.delete struct_eq s));
    2.63  
    2.64  val attribute = Attrib.syntax
    2.65       (Scan.lift ((Args.add >> K true || Args.del >> K false) --| Args.colon ||
    2.66 @@ -79,7 +74,6 @@
    2.67  (** Setup **)
    2.68  
    2.69  val setup =
    2.70 -  AlgebraData.init #>
    2.71    Method.add_methods [("algebra", Method.ctxt_args (Method.SIMPLE_METHOD' o algebra_tac),
    2.72      "normalisation of algebraic structure")] #>
    2.73    Attrib.add_attributes [("algebra", attribute, "theorems controlling algebra method")];
     3.1 --- a/src/HOL/Hyperreal/transfer.ML	Sun May 06 21:50:17 2007 +0200
     3.2 +++ b/src/HOL/Hyperreal/transfer.ML	Mon May 07 00:49:59 2007 +0200
     3.3 @@ -16,8 +16,7 @@
     3.4  struct
     3.5  
     3.6  structure TransferData = GenericDataFun
     3.7 -(struct
     3.8 -  val name = "HOL/transfer";
     3.9 +(
    3.10    type T = {
    3.11      intros: thm list,
    3.12      unfolds: thm list,
    3.13 @@ -35,8 +34,7 @@
    3.14      unfolds = Drule.merge_rules (unfolds1, unfolds2),
    3.15      refolds = Drule.merge_rules (refolds1, refolds2),
    3.16      consts = Library.merge (op =) (consts1, consts2)} : T;
    3.17 -  fun print _ _ = ();
    3.18 -end);
    3.19 +);
    3.20  
    3.21  val transfer_start = thm "transfer_start"
    3.22  
    3.23 @@ -109,7 +107,6 @@
    3.24      {intros=intros, unfolds=unfolds, refolds=refolds, consts=c::consts}))
    3.25  
    3.26  val setup =
    3.27 -  TransferData.init #>
    3.28    Attrib.add_attributes
    3.29      [("transfer_intro", Attrib.add_del_args intro_add intro_del,
    3.30        "declaration of transfer introduction rule"),
     4.1 --- a/src/HOL/Import/hol4rews.ML	Sun May 06 21:50:17 2007 +0200
     4.2 +++ b/src/HOL/Import/hol4rews.ML	Mon May 07 00:49:59 2007 +0200
     4.3 @@ -12,102 +12,70 @@
     4.4         | Generating of string
     4.5         | Replaying of string
     4.6  
     4.7 -structure HOL4DefThyArgs: THEORY_DATA_ARGS =
     4.8 -struct
     4.9 -val name = "HOL4/import_status"
    4.10 -type T = ImportStatus
    4.11 -val empty = NoImport
    4.12 -val copy = I
    4.13 -val extend = I
    4.14 -fun merge _ (NoImport,NoImport) = NoImport
    4.15 -  | merge _ _ = (warning "Import status set during merge"; NoImport)
    4.16 -fun print _ import_status =
    4.17 -    Pretty.writeln (Pretty.str (case import_status of NoImport => "No current import" | Generating thyname => ("Generating " ^ thyname) | Replaying thyname => ("Replaying " ^ thyname)))
    4.18 -end;
    4.19 -
    4.20 -structure HOL4DefThy = TheoryDataFun(HOL4DefThyArgs);
    4.21 +structure HOL4DefThy = TheoryDataFun
    4.22 +(
    4.23 +  type T = ImportStatus
    4.24 +  val empty = NoImport
    4.25 +  val copy = I
    4.26 +  val extend = I
    4.27 +  fun merge _ (NoImport,NoImport) = NoImport
    4.28 +    | merge _ _ = (warning "Import status set during merge"; NoImport)
    4.29 +)
    4.30  
    4.31 -structure ImportSegmentArgs: THEORY_DATA_ARGS =
    4.32 -struct
    4.33 -val name = "HOL4/import_segment"
    4.34 -type T = string
    4.35 -val empty = ""
    4.36 -val copy = I
    4.37 -val extend = I
    4.38 -fun merge _ ("",arg) = arg
    4.39 -  | merge _ (arg,"") = arg
    4.40 -  | merge _ (s1,s2) =
    4.41 -    if s1 = s2
    4.42 -    then s1
    4.43 -    else error "Trying to merge two different import segments"
    4.44 -fun print _ import_segment =
    4.45 -    Pretty.writeln (Pretty.str ("Import segment: " ^ import_segment))
    4.46 -end;
    4.47 -
    4.48 -structure ImportSegment = TheoryDataFun(ImportSegmentArgs);
    4.49 +structure ImportSegment = TheoryDataFun
    4.50 +(
    4.51 +  type T = string
    4.52 +  val empty = ""
    4.53 +  val copy = I
    4.54 +  val extend = I
    4.55 +  fun merge _ ("",arg) = arg
    4.56 +    | merge _ (arg,"") = arg
    4.57 +    | merge _ (s1,s2) =
    4.58 +      if s1 = s2
    4.59 +      then s1
    4.60 +      else error "Trying to merge two different import segments"
    4.61 +)
    4.62  
    4.63  val get_import_segment = ImportSegment.get
    4.64  val set_import_segment = ImportSegment.put
    4.65  
    4.66 -structure HOL4UNamesArgs: THEORY_DATA_ARGS =
    4.67 -struct
    4.68 -val name = "HOL4/used_names"
    4.69 -type T = string list
    4.70 -val empty = []
    4.71 -val copy = I
    4.72 -val extend = I
    4.73 -fun merge _ ([],[]) = []
    4.74 -  | merge _ _ = error "Used names not empty during merge"
    4.75 -fun print _ used_names =
    4.76 -    Pretty.writeln (Pretty.str "Printing of HOL4/used_names Not implemented")
    4.77 -end;
    4.78 -
    4.79 -structure HOL4UNames = TheoryDataFun(HOL4UNamesArgs);
    4.80 -
    4.81 -structure HOL4DumpArgs: THEORY_DATA_ARGS =
    4.82 -struct
    4.83 -val name = "HOL4/dump_data"
    4.84 -type T = string * string * string list
    4.85 -val empty = ("","",[])
    4.86 -val copy = I
    4.87 -val extend = I
    4.88 -fun merge _ (("","",[]),("","",[])) = ("","",[])
    4.89 -  | merge _ _ = error "Dump data not empty during merge"
    4.90 -fun print _ dump_data =
    4.91 -    Pretty.writeln (Pretty.str "Printing of HOL4/dump_data Not implemented")
    4.92 -end;
    4.93 -
    4.94 -structure HOL4Dump = TheoryDataFun(HOL4DumpArgs);
    4.95 +structure HOL4UNames = TheoryDataFun
    4.96 +(
    4.97 +  type T = string list
    4.98 +  val empty = []
    4.99 +  val copy = I
   4.100 +  val extend = I
   4.101 +  fun merge _ ([],[]) = []
   4.102 +    | merge _ _ = error "Used names not empty during merge"
   4.103 +)
   4.104  
   4.105 -structure HOL4MovesArgs: THEORY_DATA_ARGS =
   4.106 -struct
   4.107 -val name = "HOL4/moves"
   4.108 -type T = string Symtab.table
   4.109 -val empty = Symtab.empty
   4.110 -val copy = I
   4.111 -val extend = I
   4.112 -fun merge _ : T * T -> T = Symtab.merge (K true)
   4.113 -fun print _ tab =
   4.114 -  Pretty.writeln (Pretty.big_list "HOL4 moves:"
   4.115 -    (Symtab.fold (fn (bef, aft) => fn xl => (Pretty.str (bef ^ " --> " ^ aft) :: xl)) tab []))
   4.116 -end;
   4.117 -
   4.118 -structure HOL4Moves = TheoryDataFun(HOL4MovesArgs);
   4.119 +structure HOL4Dump = TheoryDataFun
   4.120 +(
   4.121 +  type T = string * string * string list
   4.122 +  val empty = ("","",[])
   4.123 +  val copy = I
   4.124 +  val extend = I
   4.125 +  fun merge _ (("","",[]),("","",[])) = ("","",[])
   4.126 +    | merge _ _ = error "Dump data not empty during merge"
   4.127 +)
   4.128  
   4.129 -structure HOL4ImportsArgs: THEORY_DATA_ARGS =
   4.130 -struct
   4.131 -val name = "HOL4/imports"
   4.132 -type T = string Symtab.table
   4.133 -val empty = Symtab.empty
   4.134 -val copy = I
   4.135 -val extend = I
   4.136 -fun merge _ : T * T -> T = Symtab.merge (K true)
   4.137 -fun print _ tab =
   4.138 -  Pretty.writeln (Pretty.big_list "HOL4 imports:"
   4.139 -    (Symtab.fold (fn (thyname, segname) => fn xl => (Pretty.str (thyname ^ " imported from segment " ^ segname) :: xl)) tab []))
   4.140 -end;
   4.141 +structure HOL4Moves = TheoryDataFun
   4.142 +(
   4.143 +  type T = string Symtab.table
   4.144 +  val empty = Symtab.empty
   4.145 +  val copy = I
   4.146 +  val extend = I
   4.147 +  fun merge _ : T * T -> T = Symtab.merge (K true)
   4.148 +)
   4.149  
   4.150 -structure HOL4Imports = TheoryDataFun(HOL4ImportsArgs);
   4.151 +structure HOL4Imports = TheoryDataFun
   4.152 +(
   4.153 +  type T = string Symtab.table
   4.154 +  val empty = Symtab.empty
   4.155 +  val copy = I
   4.156 +  val extend = I
   4.157 +  fun merge _ : T * T -> T = Symtab.merge (K true)
   4.158 +)
   4.159  
   4.160  fun get_segment2 thyname thy =
   4.161    Symtab.lookup (HOL4Imports.get thy) thyname
   4.162 @@ -120,143 +88,86 @@
   4.163  	HOL4Imports.put imps' thy
   4.164      end
   4.165  
   4.166 -structure HOL4CMovesArgs: THEORY_DATA_ARGS =
   4.167 -struct
   4.168 -val name = "HOL4/constant_moves"
   4.169 -type T = string Symtab.table
   4.170 -val empty = Symtab.empty
   4.171 -val copy = I
   4.172 -val extend = I
   4.173 -fun merge _ : T * T -> T = Symtab.merge (K true)
   4.174 -fun print _ tab =
   4.175 -  Pretty.writeln (Pretty.big_list "HOL4 constant moves:"
   4.176 -    (Symtab.fold (fn (bef, aft) => fn xl => (Pretty.str (bef ^ " --> " ^ aft) :: xl)) tab []))
   4.177 -end;
   4.178 -
   4.179 -structure HOL4CMoves = TheoryDataFun(HOL4CMovesArgs);
   4.180 +structure HOL4CMoves = TheoryDataFun
   4.181 +(
   4.182 +  type T = string Symtab.table
   4.183 +  val empty = Symtab.empty
   4.184 +  val copy = I
   4.185 +  val extend = I
   4.186 +  fun merge _ : T * T -> T = Symtab.merge (K true)
   4.187 +)
   4.188  
   4.189 -structure HOL4MapsArgs: THEORY_DATA_ARGS =
   4.190 -struct
   4.191 -val name = "HOL4/mappings"
   4.192 -type T = (string option) StringPair.table
   4.193 -val empty = StringPair.empty
   4.194 -val copy = I
   4.195 -val extend = I
   4.196 -fun merge _ : T * T -> T = StringPair.merge (K true)
   4.197 -fun print _ tab =
   4.198 -  Pretty.writeln (Pretty.big_list "HOL4 mappings:"
   4.199 -    (StringPair.fold (fn ((bthy, bthm), isathm) => fn xl =>
   4.200 -      (Pretty.str (bthy ^ "." ^ bthm ^ (case isathm of SOME th => " --> " ^ th | NONE => "IGNORED")) :: xl)) tab []))
   4.201 -end;
   4.202 -
   4.203 -structure HOL4Maps = TheoryDataFun(HOL4MapsArgs);
   4.204 +structure HOL4Maps = TheoryDataFun
   4.205 +(
   4.206 +  type T = (string option) StringPair.table
   4.207 +  val empty = StringPair.empty
   4.208 +  val copy = I
   4.209 +  val extend = I
   4.210 +  fun merge _ : T * T -> T = StringPair.merge (K true)
   4.211 +)
   4.212  
   4.213 -structure HOL4ThmsArgs: THEORY_DATA_ARGS =
   4.214 -struct
   4.215 -val name = "HOL4/theorems"
   4.216 -type T = holthm StringPair.table
   4.217 -val empty = StringPair.empty
   4.218 -val copy = I
   4.219 -val extend = I
   4.220 -fun merge _ : T * T -> T = StringPair.merge (K true)
   4.221 -fun print _ tab =
   4.222 -  Pretty.writeln (Pretty.big_list "HOL4 mappings:"
   4.223 -    (StringPair.fold (fn ((bthy, bthm), (_, thm)) => fn xl => (Pretty.str (bthy ^ "." ^ bthm ^ ":") :: Display.pretty_thm thm :: xl)) tab []))
   4.224 -end;
   4.225 -
   4.226 -structure HOL4Thms = TheoryDataFun(HOL4ThmsArgs);
   4.227 +structure HOL4Thms = TheoryDataFun
   4.228 +(
   4.229 +  type T = holthm StringPair.table
   4.230 +  val empty = StringPair.empty
   4.231 +  val copy = I
   4.232 +  val extend = I
   4.233 +  fun merge _ : T * T -> T = StringPair.merge (K true)
   4.234 +)
   4.235  
   4.236 -structure HOL4ConstMapsArgs: THEORY_DATA_ARGS =
   4.237 -struct
   4.238 -val name = "HOL4/constmappings"
   4.239 -type T = (bool * string * typ option) StringPair.table
   4.240 -val empty = StringPair.empty
   4.241 -val copy = I
   4.242 -val extend = I
   4.243 -fun merge _ : T * T -> T = StringPair.merge (K true)
   4.244 -fun print _ tab =
   4.245 -  Pretty.writeln (Pretty.big_list "HOL4 constant mappings:"
   4.246 -    (StringPair.fold (fn ((bthy, bconst), (internal, isaconst, _)) => fn xl =>
   4.247 -      (Pretty.str (bthy ^ "." ^ bconst ^ " --> " ^ isaconst ^ (if internal then " (*)" else "")) :: xl)) tab []))
   4.248 -end;
   4.249 -
   4.250 -structure HOL4ConstMaps = TheoryDataFun(HOL4ConstMapsArgs);
   4.251 +structure HOL4ConstMaps = TheoryDataFun
   4.252 +(
   4.253 +  type T = (bool * string * typ option) StringPair.table
   4.254 +  val empty = StringPair.empty
   4.255 +  val copy = I
   4.256 +  val extend = I
   4.257 +  fun merge _ : T * T -> T = StringPair.merge (K true)
   4.258 +)
   4.259  
   4.260 -structure HOL4RenameArgs: THEORY_DATA_ARGS =
   4.261 -struct
   4.262 -val name = "HOL4/renamings"
   4.263 -type T = string StringPair.table
   4.264 -val empty = StringPair.empty
   4.265 -val copy = I
   4.266 -val extend = I
   4.267 -fun merge _ : T * T -> T = StringPair.merge (K true)
   4.268 -fun print _ tab =
   4.269 -  Pretty.writeln (Pretty.big_list "HOL4 constant renamings:"
   4.270 -    (StringPair.fold (fn ((bthy,bconst),newname) => fn xl => (Pretty.str (bthy ^ "." ^ bconst ^ " --> " ^ newname)::xl)) tab []))
   4.271 -end;
   4.272 -
   4.273 -structure HOL4Rename = TheoryDataFun(HOL4RenameArgs);
   4.274 +structure HOL4Rename = TheoryDataFun
   4.275 +(
   4.276 +  type T = string StringPair.table
   4.277 +  val empty = StringPair.empty
   4.278 +  val copy = I
   4.279 +  val extend = I
   4.280 +  fun merge _ : T * T -> T = StringPair.merge (K true)
   4.281 +)
   4.282  
   4.283 -structure HOL4DefMapsArgs: THEORY_DATA_ARGS =
   4.284 -struct
   4.285 -val name = "HOL4/def_maps"
   4.286 -type T = string StringPair.table
   4.287 -val empty = StringPair.empty
   4.288 -val copy = I
   4.289 -val extend = I
   4.290 -fun merge _ : T * T -> T = StringPair.merge (K true)
   4.291 -fun print _ tab =
   4.292 -  Pretty.writeln (Pretty.big_list "HOL4 constant definitions:"
   4.293 -    (StringPair.fold (fn ((bthy,bconst),newname) => fn xl => (Pretty.str (bthy ^ "." ^ bconst ^ ": " ^ newname)::xl)) tab []))
   4.294 -end;
   4.295 -
   4.296 -structure HOL4DefMaps = TheoryDataFun(HOL4DefMapsArgs);
   4.297 +structure HOL4DefMaps = TheoryDataFun
   4.298 +(
   4.299 +  type T = string StringPair.table
   4.300 +  val empty = StringPair.empty
   4.301 +  val copy = I
   4.302 +  val extend = I
   4.303 +  fun merge _ : T * T -> T = StringPair.merge (K true)
   4.304 +)
   4.305  
   4.306 -structure HOL4TypeMapsArgs: THEORY_DATA_ARGS =
   4.307 -struct
   4.308 -val name = "HOL4/typemappings"
   4.309 -type T = (bool * string) StringPair.table
   4.310 -val empty = StringPair.empty
   4.311 -val copy = I
   4.312 -val extend = I
   4.313 -fun merge _ : T * T -> T = StringPair.merge (K true)
   4.314 -fun print _ tab =
   4.315 -  Pretty.writeln (Pretty.big_list "HOL4 type mappings:"
   4.316 -    (StringPair.fold (fn ((bthy, bconst), (internal, isaconst)) => fn xl =>
   4.317 -      (Pretty.str (bthy ^ "." ^ bconst ^ " --> " ^ isaconst ^ (if internal then " (*)" else "")) :: xl)) tab []))
   4.318 -end;
   4.319 -
   4.320 -structure HOL4TypeMaps = TheoryDataFun(HOL4TypeMapsArgs);
   4.321 +structure HOL4TypeMaps = TheoryDataFun
   4.322 +(
   4.323 +  type T = (bool * string) StringPair.table
   4.324 +  val empty = StringPair.empty
   4.325 +  val copy = I
   4.326 +  val extend = I
   4.327 +  fun merge _ : T * T -> T = StringPair.merge (K true)
   4.328 +)
   4.329  
   4.330 -structure HOL4PendingArgs: THEORY_DATA_ARGS =
   4.331 -struct
   4.332 -val name = "HOL4/pending"
   4.333 -type T = ((term * term) list * thm) StringPair.table
   4.334 -val empty = StringPair.empty
   4.335 -val copy = I
   4.336 -val extend = I
   4.337 -fun merge _ : T * T -> T = StringPair.merge (K true)
   4.338 -fun print _ tab =
   4.339 -    Pretty.writeln (Pretty.big_list "HOL4 pending theorems:"
   4.340 -	(StringPair.fold (fn ((bthy,bthm),(_,th)) => fn xl => (Pretty.chunks [Pretty.str (bthy ^ "." ^ bthm ^ ":"),Display.pretty_thm th]::xl)) tab []))
   4.341 -end;
   4.342 -
   4.343 -structure HOL4Pending = TheoryDataFun(HOL4PendingArgs);
   4.344 +structure HOL4Pending = TheoryDataFun
   4.345 +(
   4.346 +  type T = ((term * term) list * thm) StringPair.table
   4.347 +  val empty = StringPair.empty
   4.348 +  val copy = I
   4.349 +  val extend = I
   4.350 +  fun merge _ : T * T -> T = StringPair.merge (K true)
   4.351 +)
   4.352  
   4.353 -structure HOL4RewritesArgs: THEORY_DATA_ARGS =
   4.354 -struct
   4.355 -val name = "HOL4/rewrites"
   4.356 -type T = thm list
   4.357 -val empty = []
   4.358 -val copy = I
   4.359 -val extend = I
   4.360 -fun merge _ = Library.gen_union Thm.eq_thm
   4.361 -fun print _ thms =
   4.362 -    Pretty.writeln (Pretty.big_list "HOL4 rewrite rules:"
   4.363 -				    (map Display.pretty_thm thms))
   4.364 -end;
   4.365 -
   4.366 -structure HOL4Rewrites = TheoryDataFun(HOL4RewritesArgs);
   4.367 +structure HOL4Rewrites = TheoryDataFun
   4.368 +(
   4.369 +  type T = thm list
   4.370 +  val empty = []
   4.371 +  val copy = I
   4.372 +  val extend = I
   4.373 +  fun merge _ = Library.gen_union Thm.eq_thm
   4.374 +)
   4.375  
   4.376  val hol4_debug = ref false
   4.377  fun message s = if !hol4_debug then writeln s else ()
   4.378 @@ -677,7 +588,7 @@
   4.379  	  | _ => error "hol4rews.set_used_names called on initialized data!"
   4.380      end
   4.381  
   4.382 -val clear_used_names = HOL4UNames.put HOL4UNamesArgs.empty
   4.383 +val clear_used_names = HOL4UNames.put [];
   4.384  
   4.385  fun get_defmap thyname const thy =
   4.386      let
   4.387 @@ -737,21 +648,6 @@
   4.388  	    |> add_hol4_const_mapping "min" "@" false "Hilbert_Choice.Eps"
   4.389  in
   4.390  val hol4_setup =
   4.391 -  HOL4Rewrites.init #>
   4.392 -  HOL4Maps.init #>
   4.393 -  HOL4UNames.init #>
   4.394 -  HOL4DefMaps.init #>
   4.395 -  HOL4Moves.init #>
   4.396 -  HOL4CMoves.init #>
   4.397 -  HOL4ConstMaps.init #>
   4.398 -  HOL4Rename.init #>
   4.399 -  HOL4TypeMaps.init #>
   4.400 -  HOL4Pending.init #>
   4.401 -  HOL4Thms.init #>
   4.402 -  HOL4Dump.init #>
   4.403 -  HOL4DefThy.init #>
   4.404 -  HOL4Imports.init #>
   4.405 -  ImportSegment.init #>
   4.406    initial_maps #>
   4.407    Attrib.add_attributes
   4.408      [("hol4rew", Attrib.no_args add_hol4_rewrite, "HOL4 rewrite rule")]
     5.1 --- a/src/HOL/Import/import_package.ML	Sun May 06 21:50:17 2007 +0200
     5.2 +++ b/src/HOL/Import/import_package.ML	Mon May 07 00:49:59 2007 +0200
     5.3 @@ -10,18 +10,14 @@
     5.4      val debug      : bool ref
     5.5  end
     5.6  
     5.7 -structure ImportDataArgs: THEORY_DATA_ARGS =
     5.8 -struct
     5.9 -val name = "HOL4/import_data"
    5.10 -type T = ProofKernel.thm option array option
    5.11 -val empty = NONE
    5.12 -val copy = I
    5.13 -val extend = I
    5.14 -fun merge _ _ = NONE
    5.15 -fun print _ _ = ()
    5.16 -end
    5.17 -
    5.18 -structure ImportData = TheoryDataFun(ImportDataArgs)
    5.19 +structure ImportData = TheoryDataFun
    5.20 +(
    5.21 +  type T = ProofKernel.thm option array option
    5.22 +  val empty = NONE
    5.23 +  val copy = I
    5.24 +  val extend = I
    5.25 +  fun merge _ _ = NONE
    5.26 +)
    5.27  
    5.28  structure ImportPackage :> IMPORT_PACKAGE =
    5.29  struct
    5.30 @@ -80,6 +76,6 @@
    5.31                            Method.SIMPLE_METHOD (import_tac arg thy)
    5.32                        end)
    5.33  
    5.34 -val setup = Method.add_method("import",import_meth,"Import HOL4 theorem") #> ImportData.init
    5.35 +val setup = Method.add_method("import",import_meth,"Import HOL4 theorem")
    5.36  end
    5.37  
     6.1 --- a/src/HOL/Import/shuffler.ML	Sun May 06 21:50:17 2007 +0200
     6.2 +++ b/src/HOL/Import/shuffler.ML	Mon May 07 00:49:59 2007 +0200
     6.3 @@ -75,20 +75,18 @@
     6.4         | _ => raise THM("Not an equality",0,[th]))
     6.5      handle _ => raise THM("Couldn't make object equality",0,[th])
     6.6  
     6.7 -structure ShuffleDataArgs: THEORY_DATA_ARGS =
     6.8 -struct
     6.9 -val name = "HOL/shuffles"
    6.10 -type T = thm list
    6.11 -val empty = []
    6.12 -val copy = I
    6.13 -val extend = I
    6.14 -fun merge _ = Library.gen_union Thm.eq_thm
    6.15 -fun print _ thms =
    6.16 -    Pretty.writeln (Pretty.big_list "Shuffle theorems:"
    6.17 -                                    (map Display.pretty_thm thms))
    6.18 -end
    6.19 +structure ShuffleData = TheoryDataFun
    6.20 +(
    6.21 +  type T = thm list
    6.22 +  val empty = []
    6.23 +  val copy = I
    6.24 +  val extend = I
    6.25 +  fun merge _ = Library.gen_union Thm.eq_thm
    6.26 +)
    6.27  
    6.28 -structure ShuffleData = TheoryDataFun(ShuffleDataArgs)
    6.29 +fun print_shuffles thy =
    6.30 +  Pretty.writeln (Pretty.big_list "Shuffle theorems:"
    6.31 +    (map Display.pretty_thm (ShuffleData.get thy)))
    6.32  
    6.33  val weaken =
    6.34      let
    6.35 @@ -667,8 +665,6 @@
    6.36          Method.SIMPLE_METHOD' (gen_shuffle_tac thy true (map (pair "premise") prems))
    6.37      end
    6.38  
    6.39 -val print_shuffles = ShuffleData.print
    6.40 -
    6.41  fun add_shuffle_rule thm thy =
    6.42      let
    6.43          val shuffles = ShuffleData.get thy
    6.44 @@ -682,9 +678,10 @@
    6.45  val shuffle_attr = Thm.declaration_attribute (fn th => Context.mapping (add_shuffle_rule th) I);
    6.46  
    6.47  val setup =
    6.48 -  Method.add_method ("shuffle_tac",Method.thms_ctxt_args shuffle_meth,"solve goal by shuffling terms around") #>
    6.49 -  Method.add_method ("search_tac",Method.ctxt_args search_meth,"search for suitable theorems") #>
    6.50 -  ShuffleData.init #>
    6.51 +  Method.add_method ("shuffle_tac",
    6.52 +    Method.thms_ctxt_args shuffle_meth,"solve goal by shuffling terms around") #>
    6.53 +  Method.add_method ("search_tac",
    6.54 +    Method.ctxt_args search_meth,"search for suitable theorems") #>
    6.55    add_shuffle_rule weaken #>
    6.56    add_shuffle_rule equiv_comm #>
    6.57    add_shuffle_rule imp_comm #>
     7.1 --- a/src/HOL/Inductive.thy	Sun May 06 21:50:17 2007 +0200
     7.2 +++ b/src/HOL/Inductive.thy	Mon May 07 00:49:59 2007 +0200
     7.3 @@ -118,7 +118,6 @@
     7.4  use "Tools/datatype_realizer.ML"
     7.5  
     7.6  use "Tools/datatype_hooks.ML"
     7.7 -setup DatatypeHooks.setup
     7.8  
     7.9  use "Tools/datatype_package.ML"
    7.10  setup DatatypePackage.setup
     8.1 --- a/src/HOL/Nominal/Nominal.thy	Sun May 06 21:50:17 2007 +0200
     8.2 +++ b/src/HOL/Nominal/Nominal.thy	Mon May 07 00:49:59 2007 +0200
     8.3 @@ -3226,7 +3226,6 @@
     8.4  (* setup for the individial atom-kinds *)
     8.5  (* and nominal datatypes               *)
     8.6  use "nominal_atoms.ML"
     8.7 -setup "NominalAtoms.setup"
     8.8  
     8.9  (************************************************************)
    8.10  (* various tactics for analysing permutations, supports etc *)
    8.11 @@ -3288,7 +3287,6 @@
    8.12  (************************************************)
    8.13  (* main file for constructing nominal datatypes *)
    8.14  use "nominal_package.ML"
    8.15 -setup "NominalPackage.setup"
    8.16  
    8.17  (******************************************************)
    8.18  (* primitive recursive functions on nominal datatypes *)
     9.1 --- a/src/HOL/Nominal/nominal_atoms.ML	Sun May 06 21:50:17 2007 +0200
     9.2 +++ b/src/HOL/Nominal/nominal_atoms.ML	Mon May 07 00:49:59 2007 +0200
     9.3 @@ -13,7 +13,6 @@
     9.4    val get_atom_info : theory -> string -> atom_info option
     9.5    val atoms_of : theory -> string list
     9.6    val mk_permT : typ -> typ
     9.7 -  val setup : theory -> theory
     9.8  end
     9.9  
    9.10  structure NominalAtoms : NOMINAL_ATOMS =
    9.11 @@ -23,27 +22,21 @@
    9.12  val Collect_const = thm "Collect_const";
    9.13  
    9.14  
    9.15 -(* data kind 'HOL/nominal' *)
    9.16 +(* theory data *)
    9.17  
    9.18  type atom_info =
    9.19    {pt_class : string,
    9.20     fs_class : string,
    9.21     cp_classes : (string * string) list};
    9.22  
    9.23 -structure NominalArgs =
    9.24 -struct
    9.25 -  val name = "HOL/nominal";
    9.26 +structure NominalData = TheoryDataFun
    9.27 +(
    9.28    type T = atom_info Symtab.table;
    9.29 -
    9.30    val empty = Symtab.empty;
    9.31    val copy = I;
    9.32    val extend = I;
    9.33    fun merge _ x = Symtab.merge (K true) x;
    9.34 -
    9.35 -  fun print sg tab = ();
    9.36 -end;
    9.37 -
    9.38 -structure NominalData = TheoryDataFun(NominalArgs);
    9.39 +);
    9.40  
    9.41  fun make_atom_info ((pt_class, fs_class), cp_classes) =
    9.42    {pt_class = pt_class,
    9.43 @@ -889,6 +882,4 @@
    9.44  
    9.45  val _ = OuterSyntax.add_parsers [atom_declP];
    9.46  
    9.47 -val setup = NominalData.init;
    9.48 -
    9.49  end;
    10.1 --- a/src/HOL/Nominal/nominal_package.ML	Sun May 06 21:50:17 2007 +0200
    10.2 +++ b/src/HOL/Nominal/nominal_package.ML	Mon May 07 00:49:59 2007 +0200
    10.3 @@ -17,7 +17,6 @@
    10.4    val perm_of_pair: term * term -> term
    10.5    val mk_not_sym: thm list -> thm list
    10.6    val perm_simproc: simproc
    10.7 -  val setup: theory -> theory
    10.8  end
    10.9  
   10.10  structure NominalPackage : NOMINAL_PACKAGE =
   10.11 @@ -68,7 +67,7 @@
   10.12  
   10.13  end;
   10.14  
   10.15 -(* data kind 'HOL/nominal_datatypes' *)
   10.16 +(* theory data *)
   10.17  
   10.18  type descr = (int * (string * dtyp list * (string * (dtyp list * dtyp) list) list)) list;
   10.19  
   10.20 @@ -83,25 +82,19 @@
   10.21     inject : thm list};
   10.22  
   10.23  structure NominalDatatypesData = TheoryDataFun
   10.24 -(struct
   10.25 -  val name = "HOL/nominal_datatypes";
   10.26 +(
   10.27    type T = nominal_datatype_info Symtab.table;
   10.28 -
   10.29    val empty = Symtab.empty;
   10.30    val copy = I;
   10.31    val extend = I;
   10.32    fun merge _ tabs : T = Symtab.merge (K true) tabs;
   10.33 -
   10.34 -  fun print sg tab =
   10.35 -    Pretty.writeln (Pretty.strs ("nominal datatypes:" ::
   10.36 -      map #1 (NameSpace.extern_table (Sign.type_space sg, tab))));
   10.37 -end);
   10.38 +);
   10.39  
   10.40  val get_nominal_datatypes = NominalDatatypesData.get;
   10.41  val put_nominal_datatypes = NominalDatatypesData.put;
   10.42  val map_nominal_datatypes = NominalDatatypesData.map;
   10.43  val get_nominal_datatype = Symtab.lookup o get_nominal_datatypes;
   10.44 -val setup = NominalDatatypesData.init;
   10.45 +
   10.46  
   10.47  (**** make datatype info ****)
   10.48  
    11.1 --- a/src/HOL/Nominal/nominal_thmdecls.ML	Sun May 06 21:50:17 2007 +0200
    11.2 +++ b/src/HOL/Nominal/nominal_thmdecls.ML	Mon May 07 00:49:59 2007 +0200
    11.3 @@ -1,13 +1,13 @@
    11.4  (* ID: "$Id$"
    11.5     Authors: Julien Narboux and Christian Urban
    11.6  
    11.7 -   This file introduces the infrastructure for the lemma 
    11.8 +   This file introduces the infrastructure for the lemma
    11.9     declaration "eqvts" "bijs" and "freshs".
   11.10  
   11.11 -   By attaching [eqvt] [bij] or [fresh] to a lemma, the lemma gets stored 
   11.12 +   By attaching [eqvt] [bij] or [fresh] to a lemma, the lemma gets stored
   11.13     in a data-slot in the theory context. Possible modifiers
   11.14     are [attribute add] and [attribute del] for adding and deleting,
   11.15 -   respectively the lemma from the data-slot.  
   11.16 +   respectively the lemma from the data-slot.
   11.17  *)
   11.18  
   11.19  signature NOMINAL_THMDECLS =
   11.20 @@ -21,7 +21,7 @@
   11.21    val get_eqvt_thms: theory -> thm list
   11.22    val get_fresh_thms: theory -> thm list
   11.23    val get_bij_thms: theory -> thm list
   11.24 -  
   11.25 +
   11.26  
   11.27    val NOMINAL_EQVT_DEBUG : bool ref
   11.28  end;
   11.29 @@ -31,24 +31,12 @@
   11.30  
   11.31  structure Data = GenericDataFun
   11.32  (
   11.33 -  val name = "HOL/Nominal/eqvt";
   11.34    type T = {eqvts:thm list, freshs:thm list, bijs:thm list};
   11.35    val empty = ({eqvts=[], freshs=[], bijs=[]}:T);
   11.36    val extend = I;
   11.37 -  fun merge _ (r1:T,r2:T) = {eqvts  = Drule.merge_rules (#eqvts r1, #eqvts r2), 
   11.38 -                             freshs = Drule.merge_rules (#freshs r1, #freshs r2), 
   11.39 +  fun merge _ (r1:T,r2:T) = {eqvts  = Drule.merge_rules (#eqvts r1, #eqvts r2),
   11.40 +                             freshs = Drule.merge_rules (#freshs r1, #freshs r2),
   11.41                               bijs   = Drule.merge_rules (#bijs r1, #bijs r2)}
   11.42 -  fun print context (data:T) =
   11.43 -    let 
   11.44 -       fun print_aux msg thms =
   11.45 -         Pretty.writeln (Pretty.big_list msg
   11.46 -           (map (ProofContext.pretty_thm (Context.proof_of context)) thms))
   11.47 -    in
   11.48 -      (print_aux "Equivariance lemmas: " (#eqvts data);
   11.49 -       print_aux "Freshness lemmas: " (#freshs data);
   11.50 -       print_aux "Bijection lemmas: " (#bijs data))
   11.51 -    end;
   11.52 - 
   11.53  );
   11.54  
   11.55  (* Exception for when a theorem does not conform with form of an equivariance lemma. *)
   11.56 @@ -62,7 +50,19 @@
   11.57  (* eqality-lemma can be derived. *)
   11.58  exception EQVT_FORM of string;
   11.59  
   11.60 -val print_data = Data.print o Context.Proof;
   11.61 +fun print_data ctxt =
   11.62 +  let
   11.63 +    val data = Data.get (Context.Proof ctxt);
   11.64 +    fun pretty_thms msg thms =
   11.65 +      Pretty.big_list msg (map (ProofContext.pretty_thm ctxt) thms);
   11.66 +  in
   11.67 +    Pretty.writeln (Pretty.chunks
   11.68 +     [pretty_thms "Equivariance lemmas:" (#eqvts data),
   11.69 +      pretty_thms "Freshness lemmas:" (#freshs data),
   11.70 +      pretty_thms "Bijection lemmas:" (#bijs data)])
   11.71 +  end;
   11.72 +
   11.73 +
   11.74  val get_eqvt_thms = Context.Theory #> Data.get #> #eqvts;
   11.75  val get_fresh_thms = Context.Theory #> Data.get #> #freshs;
   11.76  val get_bij_thms = Context.Theory #> Data.get #> #bijs;
   11.77 @@ -75,56 +75,56 @@
   11.78  
   11.79  val NOMINAL_EQVT_DEBUG = ref false;
   11.80  
   11.81 -fun tactic (msg,tac) = 
   11.82 -    if !NOMINAL_EQVT_DEBUG 
   11.83 +fun tactic (msg,tac) =
   11.84 +    if !NOMINAL_EQVT_DEBUG
   11.85      then (EVERY [tac, print_tac ("after "^msg)])
   11.86 -    else tac 
   11.87 +    else tac
   11.88  
   11.89  fun dynamic_thms thy name = PureThy.get_thms thy (Name name)
   11.90  
   11.91 -fun tactic_eqvt ctx orig_thm pi typi = 
   11.92 -    let 
   11.93 +fun tactic_eqvt ctx orig_thm pi typi =
   11.94 +    let
   11.95          val mypi = Thm.cterm_of ctx (Var (pi,typi))
   11.96          val mypifree = Thm.cterm_of ctx (Const ("List.rev",typi --> typi) $ Free (fst pi,typi))
   11.97          val perm_pi_simp = dynamic_thms ctx "perm_pi_simp"
   11.98      in
   11.99 -        EVERY [tactic ("iffI applied",rtac iffI 1), 
  11.100 -               tactic ("simplifies with orig_thm and perm_bool", 
  11.101 -                          asm_full_simp_tac (HOL_basic_ss addsimps [perm_bool,orig_thm]) 1), 
  11.102 +        EVERY [tactic ("iffI applied",rtac iffI 1),
  11.103 +               tactic ("simplifies with orig_thm and perm_bool",
  11.104 +                          asm_full_simp_tac (HOL_basic_ss addsimps [perm_bool,orig_thm]) 1),
  11.105                 tactic ("applies orig_thm instantiated with rev pi",
  11.106 -                          dtac (Drule.cterm_instantiate [(mypi,mypifree)] orig_thm) 1), 
  11.107 +                          dtac (Drule.cterm_instantiate [(mypi,mypifree)] orig_thm) 1),
  11.108                 tactic ("getting rid of all remaining perms",
  11.109 -                          full_simp_tac (HOL_basic_ss addsimps (perm_bool::perm_pi_simp)) 1)] 
  11.110 +                          full_simp_tac (HOL_basic_ss addsimps (perm_bool::perm_pi_simp)) 1)]
  11.111      end;
  11.112  
  11.113  fun get_derived_thm thy hyp concl orig_thm pi typi =
  11.114 -   let 
  11.115 +   let
  11.116         val lhs = (Const("Nominal.perm", typi --> HOLogic.boolT --> HOLogic.boolT) $ Var(pi,typi) $ hyp)
  11.117 -       val goal_term = Logic.unvarify (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs,concl))) 
  11.118 -       val _ = Display.print_cterm (cterm_of thy goal_term) 
  11.119 +       val goal_term = Logic.unvarify (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs,concl)))
  11.120 +       val _ = Display.print_cterm (cterm_of thy goal_term)
  11.121     in	
  11.122 -     Goal.prove_global thy [] [] goal_term (fn _ => (tactic_eqvt thy orig_thm pi typi)) 
  11.123 +     Goal.prove_global thy [] [] goal_term (fn _ => (tactic_eqvt thy orig_thm pi typi))
  11.124     end
  11.125  
  11.126  (* FIXME: something naughty here, but as long as there is no infrastructure to expose *)
  11.127  (* the eqvt_thm_list to the user, we have to manually update the context and the      *)
  11.128  (* thm-list eqvt *)
  11.129  fun update_context flag thms context =
  11.130 -  let 
  11.131 -     val context' = fold (fn thm => Data.map (flag thm)) thms context 
  11.132 -  in 
  11.133 +  let
  11.134 +     val context' = fold (fn thm => Data.map (flag thm)) thms context
  11.135 +  in
  11.136      Context.mapping (snd o PureThy.add_thmss [(("eqvts",(#eqvts (Data.get context'))),[])]) I context'
  11.137    end;
  11.138  
  11.139 -(* replaces every variable x in t with pi o x *) 
  11.140 +(* replaces every variable x in t with pi o x *)
  11.141  fun apply_pi trm (pi,typi) =
  11.142 -  let 
  11.143 +  let
  11.144      fun only_vars t =
  11.145         (case t of
  11.146            Var (n,ty) => (Const ("Nominal.perm",typi --> ty --> ty) $ (Var (pi,typi)) $ (Var (n,ty)))
  11.147          | _ => t)
  11.148 -  in 
  11.149 -     map_aterms only_vars trm 
  11.150 +  in
  11.151 +     map_aterms only_vars trm
  11.152    end;
  11.153  
  11.154  (* returns *the* pi which is in front of all variables, provided there *)
  11.155 @@ -132,69 +132,69 @@
  11.156  fun get_pi t thy =
  11.157    let fun get_pi_aux s =
  11.158          (case s of
  11.159 -          (Const ("Nominal.perm",typrm) $ 
  11.160 -             (Var (pi,typi as Type("List.list",[Type ("*",[Type (tyatm,[]),_])]))) $ 
  11.161 -               (Var (n,ty))) => 
  11.162 +          (Const ("Nominal.perm",typrm) $
  11.163 +             (Var (pi,typi as Type("List.list",[Type ("*",[Type (tyatm,[]),_])]))) $
  11.164 +               (Var (n,ty))) =>
  11.165               let
  11.166  		(* FIXME: this should be an operation the library *)
  11.167 -                val class_name = (NameSpace.map_base (fn s => "pt_"^s) tyatm) 
  11.168 -	     in 
  11.169 -		if (Type.of_sort (Sign.tsig_of thy) (ty,[class_name])) 
  11.170 -                then [(pi,typi)] 
  11.171 -                else raise 
  11.172 -                EQVT_FORM ("Could not find any permutation or an argument is not an instance of "^class_name) 
  11.173 -             end 
  11.174 +                val class_name = (NameSpace.map_base (fn s => "pt_"^s) tyatm)
  11.175 +	     in
  11.176 +		if (Type.of_sort (Sign.tsig_of thy) (ty,[class_name]))
  11.177 +                then [(pi,typi)]
  11.178 +                else raise
  11.179 +                EQVT_FORM ("Could not find any permutation or an argument is not an instance of "^class_name)
  11.180 +             end
  11.181          | Abs (_,_,t1) => get_pi_aux t1
  11.182          | (t1 $ t2) => get_pi_aux t1 @ get_pi_aux t2
  11.183 -        | _ => [])  
  11.184 -  in 
  11.185 +        | _ => [])
  11.186 +  in
  11.187      (* collect first all pi's in front of variables in t and then use distinct *)
  11.188      (* to ensure that all pi's must have been the same, i.e. distinct returns  *)
  11.189      (* a singleton-list  *)
  11.190 -    (case (distinct (op =) (get_pi_aux t)) of 
  11.191 +    (case (distinct (op =) (get_pi_aux t)) of
  11.192        [(pi,typi)] => (pi,typi)
  11.193      | _ => raise EQVT_FORM "All permutation should be the same")
  11.194    end;
  11.195  
  11.196  (* Either adds a theorem (orig_thm) to or deletes one from the equivaraince *)
  11.197  (* lemma list depending on flag. To be added the lemma has to satisfy a     *)
  11.198 -(* certain form. *) 
  11.199 +(* certain form. *)
  11.200  fun eqvt_add_del_aux flag orig_thm context =
  11.201 -  let 
  11.202 +  let
  11.203      val thy = Context.theory_of context
  11.204      val thms_to_be_added = (case (prop_of orig_thm) of
  11.205 -        (* case: eqvt-lemma is of the implicational form *) 
  11.206 +        (* case: eqvt-lemma is of the implicational form *)
  11.207          (Const("==>", _) $ (Const ("Trueprop",_) $ hyp) $ (Const ("Trueprop",_) $ concl)) =>
  11.208 -          let  
  11.209 +          let
  11.210              val (pi,typi) = get_pi concl thy
  11.211            in
  11.212               if (apply_pi hyp (pi,typi) = concl)
  11.213 -             then 
  11.214 +             then
  11.215                 (warning ("equivariance lemma of the relational form");
  11.216                  [orig_thm, get_derived_thm thy hyp concl orig_thm pi typi])
  11.217               else raise EQVT_FORM "Type Implication"
  11.218            end
  11.219 -       (* case: eqvt-lemma is of the equational form *)  
  11.220 -      | (Const ("Trueprop", _) $ (Const ("op =", _) $ 
  11.221 +       (* case: eqvt-lemma is of the equational form *)
  11.222 +      | (Const ("Trueprop", _) $ (Const ("op =", _) $
  11.223              (Const ("Nominal.perm",typrm) $ Var (pi,typi) $ lhs) $ rhs)) =>
  11.224 -	   (if (apply_pi lhs (pi,typi)) = rhs 
  11.225 +	   (if (apply_pi lhs (pi,typi)) = rhs
  11.226                 then [orig_thm]
  11.227                 else raise EQVT_FORM "Type Equality")
  11.228        | _ => raise EQVT_FORM "Type unknown")
  11.229 -  in 
  11.230 +  in
  11.231        update_context flag thms_to_be_added context
  11.232    end
  11.233 -  handle EQVT_FORM s => 
  11.234 +  handle EQVT_FORM s =>
  11.235        error (string_of_thm orig_thm ^ " does not comply with the form of an equivariance lemma ("^s^").")
  11.236  
  11.237  (* in cases of bij- and freshness, we just add the lemmas to the *)
  11.238 -(* data-slot *) 
  11.239 +(* data-slot *)
  11.240  
  11.241 -fun simple_add_del_aux record_access name flag th context = 
  11.242 -   let 
  11.243 +fun simple_add_del_aux record_access name flag th context =
  11.244 +   let
  11.245       val context' = Data.map (flag th) context
  11.246     in
  11.247 -     Context.mapping (snd o PureThy.add_thmss [((name,(record_access (Data.get context'))),[])]) I context' 
  11.248 +     Context.mapping (snd o PureThy.add_thmss [((name,(record_access (Data.get context'))),[])]) I context'
  11.249     end
  11.250  
  11.251  fun bij_add_del_aux f   = simple_add_del_aux #bijs "bijs" f
  11.252 @@ -205,21 +205,20 @@
  11.253  fun fresh_map f th (r:Data.T) = {eqvts = #eqvts r, freshs = (f th (#freshs r)), bijs = #bijs r};
  11.254  fun bij_map f th (r:Data.T)   = {eqvts = #eqvts r, freshs = #freshs r, bijs = (f th (#bijs r))};
  11.255  
  11.256 -val eqvt_add  = Thm.declaration_attribute (eqvt_add_del_aux (eqvt_map Drule.add_rule)); 
  11.257 -val eqvt_del  = Thm.declaration_attribute (eqvt_add_del_aux (eqvt_map Drule.del_rule)); 
  11.258 -val eqvt_force_add  = Thm.declaration_attribute (eqvt_force_add_del_aux (eqvt_map Drule.add_rule)); 
  11.259 -val eqvt_force_del  = Thm.declaration_attribute (eqvt_force_add_del_aux (eqvt_map Drule.del_rule)); 
  11.260 +val eqvt_add  = Thm.declaration_attribute (eqvt_add_del_aux (eqvt_map Drule.add_rule));
  11.261 +val eqvt_del  = Thm.declaration_attribute (eqvt_add_del_aux (eqvt_map Drule.del_rule));
  11.262 +val eqvt_force_add  = Thm.declaration_attribute (eqvt_force_add_del_aux (eqvt_map Drule.add_rule));
  11.263 +val eqvt_force_del  = Thm.declaration_attribute (eqvt_force_add_del_aux (eqvt_map Drule.del_rule));
  11.264  
  11.265 -val bij_add   = Thm.declaration_attribute (bij_add_del_aux (bij_map Drule.add_rule)); 
  11.266 +val bij_add   = Thm.declaration_attribute (bij_add_del_aux (bij_map Drule.add_rule));
  11.267  val bij_del   = Thm.declaration_attribute (bij_add_del_aux (bij_map Drule.del_rule));
  11.268 -val fresh_add = Thm.declaration_attribute (fresh_add_del_aux (fresh_map Drule.add_rule)); 
  11.269 +val fresh_add = Thm.declaration_attribute (fresh_add_del_aux (fresh_map Drule.add_rule));
  11.270  val fresh_del = Thm.declaration_attribute (fresh_add_del_aux (fresh_map Drule.del_rule));
  11.271  
  11.272  
  11.273  
  11.274  val setup =
  11.275 -  Data.init #>
  11.276 -  Attrib.add_attributes 
  11.277 +  Attrib.add_attributes
  11.278       [("eqvt",  Attrib.add_del_args eqvt_add eqvt_del,   "equivariance theorem declaration"),
  11.279        ("eqvt_force", Attrib.add_del_args eqvt_force_add eqvt_force_del,
  11.280                               "equivariance theorem declaration (without checking the form of the lemma)"),
  11.281 @@ -227,11 +226,3 @@
  11.282        ("bij",   Attrib.add_del_args bij_add bij_del,     "bijection theorem declaration")];
  11.283  
  11.284  end;
  11.285 -
  11.286 -(* Thm.declaration_attribute has type (thm -> Context.generic -> Context.generic) -> attribute *)
  11.287 -
  11.288 -(* Drule.add_rule has type thm -> thm list -> thm list *)
  11.289 -
  11.290 -(* Data.map has type thm list -> thm list -> Context.generic -> Context.generic *)
  11.291 -
  11.292 -(* add_del_args is of type attribute -> attribute -> src -> attribute *)
  11.293 \ No newline at end of file
    12.1 --- a/src/HOL/Predicate.thy	Sun May 06 21:50:17 2007 +0200
    12.2 +++ b/src/HOL/Predicate.thy	Mon May 07 00:49:59 2007 +0200
    12.3 @@ -152,14 +152,12 @@
    12.4  val rules2 = [split_set, mk_meta_eq mem_Collect_eq, mem_Collect2_eq];
    12.5  
    12.6  structure PredSetConvData = GenericDataFun
    12.7 -(struct
    12.8 -  val name = "HOL/pred_set_conv";
    12.9 +(
   12.10    type T = thm list;
   12.11    val empty = [];
   12.12    val extend = I;
   12.13    fun merge _ = Drule.merge_rules;
   12.14 -  fun print _ _ = ()
   12.15 -end)
   12.16 +);
   12.17  
   12.18  fun mk_attr ths1 ths2 f = Attrib.syntax (Attrib.thms >> (fn ths =>
   12.19    Thm.rule_attribute (fn ctxt => rew ths1 (map (f o Simpdata.mk_eq)
   12.20 @@ -170,7 +168,7 @@
   12.21  
   12.22  in
   12.23  
   12.24 -val _ = ML_Context.>> (PredSetConvData.init #>
   12.25 +val _ = ML_Context.>> (
   12.26    Attrib.add_attributes
   12.27      [("pred_set_conv", pred_set_conv_att,
   12.28          "declare rules for converting between predicate and set notation"),
    13.1 --- a/src/HOL/Tools/datatype_hooks.ML	Sun May 06 21:50:17 2007 +0200
    13.2 +++ b/src/HOL/Tools/datatype_hooks.ML	Mon May 07 00:49:59 2007 +0200
    13.3 @@ -7,49 +7,29 @@
    13.4  
    13.5  signature DATATYPE_HOOKS =
    13.6  sig
    13.7 -  type hook = string list -> theory -> theory;
    13.8 -  val add: hook -> theory -> theory;
    13.9 -  val all: hook;
   13.10 -  val setup: theory -> theory;
   13.11 +  type hook = string list -> theory -> theory
   13.12 +  val add: hook -> theory -> theory
   13.13 +  val all: hook
   13.14  end;
   13.15  
   13.16  structure DatatypeHooks : DATATYPE_HOOKS =
   13.17  struct
   13.18  
   13.19 -
   13.20 -(* theory data *)
   13.21 -
   13.22  type hook = string list -> theory -> theory;
   13.23 -datatype T = T of (serial * hook) list;
   13.24 -
   13.25 -fun map_T f (T hooks) = T (f hooks);
   13.26 -fun merge_T pp (T hooks1, T hooks2) =
   13.27 -  T (AList.merge (op =) (K true) (hooks1, hooks2));
   13.28  
   13.29  structure DatatypeHooksData = TheoryDataFun
   13.30 -(struct
   13.31 -  val name = "HOL/datatype_hooks";
   13.32 -  type T = T;
   13.33 -  val empty = T [];
   13.34 +(
   13.35 +  type T = (serial * hook) list;
   13.36 +  val empty = [];
   13.37    val copy = I;
   13.38    val extend = I;
   13.39 -  val merge = merge_T;
   13.40 -  fun print _ _ = ();
   13.41 -end);
   13.42 -
   13.43 -
   13.44 -(* interface *)
   13.45 +  fun merge _ hooks : T = AList.merge (op =) (K true) hooks;
   13.46 +);
   13.47  
   13.48  fun add hook =
   13.49 -  DatatypeHooksData.map (map_T (cons (serial (), hook)));
   13.50 +  DatatypeHooksData.map (cons (serial (), hook));
   13.51  
   13.52  fun all dtcos thy =
   13.53 -  fold (fn (_, f) => f dtcos) ((fn T hooks => hooks) (DatatypeHooksData.get thy)) thy;
   13.54 -
   13.55 -
   13.56 -(* theory setup *)
   13.57 -
   13.58 -val setup = DatatypeHooksData.init;
   13.59 +  fold (fn (_, f) => f dtcos) (DatatypeHooksData.get thy) thy;
   13.60  
   13.61  end;
   13.62 -
    14.1 --- a/src/HOL/Tools/datatype_package.ML	Sun May 06 21:50:17 2007 +0200
    14.2 +++ b/src/HOL/Tools/datatype_package.ML	Mon May 07 00:49:59 2007 +0200
    14.3 @@ -85,11 +85,10 @@
    14.4  val quiet_mode = quiet_mode;
    14.5  
    14.6  
    14.7 -(* data kind 'HOL/datatypes' *)
    14.8 +(* theory data *)
    14.9  
   14.10  structure DatatypesData = TheoryDataFun
   14.11 -(struct
   14.12 -  val name = "HOL/datatypes";
   14.13 +(
   14.14    type T =
   14.15      {types: datatype_info Symtab.table,
   14.16       constrs: datatype_info Symtab.table,
   14.17 @@ -105,15 +104,14 @@
   14.18      {types = Symtab.merge (K true) (types1, types2),
   14.19       constrs = Symtab.merge (K true) (constrs1, constrs2),
   14.20       cases = Symtab.merge (K true) (cases1, cases2)};
   14.21 -
   14.22 -  fun print sg ({types, ...} : T) =
   14.23 -    Pretty.writeln (Pretty.strs ("datatypes:" ::
   14.24 -      map #1 (NameSpace.extern_table (Sign.type_space sg, types))));
   14.25 -end);
   14.26 +);
   14.27  
   14.28  val get_datatypes = #types o DatatypesData.get;
   14.29  val map_datatypes = DatatypesData.map;
   14.30 -val print_datatypes = DatatypesData.print;
   14.31 +
   14.32 +fun print_datatypes thy =
   14.33 +  Pretty.writeln (Pretty.strs ("datatypes:" ::
   14.34 +    map #1 (NameSpace.extern_table (Sign.type_space thy, get_datatypes thy))));
   14.35  
   14.36  
   14.37  (** theory information about datatypes **)
   14.38 @@ -933,7 +931,7 @@
   14.39  (* setup theory *)
   14.40  
   14.41  val setup =
   14.42 -  DatatypesData.init #> Method.add_methods tactic_emulations #> simproc_setup #> trfun_setup;
   14.43 +  Method.add_methods tactic_emulations #> simproc_setup #> trfun_setup;
   14.44  
   14.45  
   14.46  (* outer syntax *)
    15.1 --- a/src/HOL/Tools/function_package/fundef_common.ML	Sun May 06 21:50:17 2007 +0200
    15.2 +++ b/src/HOL/Tools/function_package/fundef_common.ML	Mon May 07 00:49:59 2007 +0200
    15.3 @@ -78,30 +78,24 @@
    15.4      end
    15.5  
    15.6  structure FundefData = GenericDataFun
    15.7 -(struct
    15.8 -  val name = "HOL/function_def/data";
    15.9 -  type T = (term * fundef_context_data) NetRules.T
   15.10 -
   15.11 +(
   15.12 +  type T = (term * fundef_context_data) NetRules.T;
   15.13    val empty = NetRules.init
   15.14      (op aconv o pairself fst : (term * fundef_context_data) * (term * fundef_context_data) -> bool)
   15.15      fst;
   15.16    val copy = I;
   15.17    val extend = I;
   15.18    fun merge _ (tab1, tab2) = NetRules.merge (tab1, tab2)
   15.19 -
   15.20 -  fun print _ _ = ();
   15.21 -end);
   15.22 +);
   15.23  
   15.24  
   15.25  structure FundefCongs = GenericDataFun
   15.26 -(struct
   15.27 -    val name = "HOL/function_def/congs"
   15.28 -    type T = thm list
   15.29 -    val empty = []
   15.30 -    val extend = I
   15.31 -    fun merge _ = Drule.merge_rules
   15.32 -    fun print  _ _ = ()
   15.33 -end);
   15.34 +(
   15.35 +  type T = thm list
   15.36 +  val empty = []
   15.37 +  val extend = I
   15.38 +  fun merge _ = Drule.merge_rules
   15.39 +);
   15.40  
   15.41  
   15.42  (* Generally useful?? *)
   15.43 @@ -143,14 +137,12 @@
   15.44  
   15.45  
   15.46  structure TerminationRule = GenericDataFun
   15.47 -(struct
   15.48 -    val name = "HOL/function_def/termination"
   15.49 -    type T = thm list
   15.50 -    val empty = []
   15.51 -    val extend = I
   15.52 -    fun merge _ = Drule.merge_rules
   15.53 -    fun print  _ _ = ()
   15.54 -end);
   15.55 +(
   15.56 +  type T = thm list
   15.57 +  val empty = []
   15.58 +  val extend = I
   15.59 +  fun merge _ = Drule.merge_rules
   15.60 +);
   15.61  
   15.62  val get_termination_rules = TerminationRule.get
   15.63  val store_termination_rule = TerminationRule.map o cons
    16.1 --- a/src/HOL/Tools/function_package/fundef_package.ML	Sun May 06 21:50:17 2007 +0200
    16.2 +++ b/src/HOL/Tools/function_package/fundef_package.ML	Mon May 07 00:49:59 2007 +0200
    16.3 @@ -208,13 +208,11 @@
    16.4  (* setup *)
    16.5  
    16.6  val setup =
    16.7 -    FundefData.init
    16.8 -      #> FundefCongs.init
    16.9 -      #> TerminationRule.init
   16.10 -      #>  Attrib.add_attributes
   16.11 -            [("fundef_cong", Attrib.add_del_args cong_add cong_del, "declaration of congruence rule for function definitions")]
   16.12 -      #> setup_case_cong_hook
   16.13 -      #> FundefRelation.setup
   16.14 +  Attrib.add_attributes
   16.15 +    [("fundef_cong", Attrib.add_del_args cong_add cong_del,
   16.16 +      "declaration of congruence rule for function definitions")]
   16.17 +  #> setup_case_cong_hook
   16.18 +  #> FundefRelation.setup
   16.19  
   16.20  val get_congs = FundefCommon.get_fundef_congs o Context.Theory
   16.21  
    17.1 --- a/src/HOL/Tools/inductive_codegen.ML	Sun May 06 21:50:17 2007 +0200
    17.2 +++ b/src/HOL/Tools/inductive_codegen.ML	Mon May 07 00:49:59 2007 +0200
    17.3 @@ -22,8 +22,7 @@
    17.4    Symtab.join (fn _ => AList.merge (Thm.eq_thm_prop) (K true)) tabs;
    17.5  
    17.6  structure CodegenData = TheoryDataFun
    17.7 -(struct
    17.8 -  val name = "HOL/inductive_codegen";
    17.9 +(
   17.10    type T =
   17.11      {intros : (thm * (string * int)) list Symtab.table,
   17.12       graph : unit Graph.T,
   17.13 @@ -37,8 +36,7 @@
   17.14      {intros = merge_rules (intros1, intros2),
   17.15       graph = Graph.merge (K true) (graph1, graph2),
   17.16       eqns = merge_rules (eqns1, eqns2)};
   17.17 -  fun print _ _ = ();
   17.18 -end);
   17.19 +);
   17.20  
   17.21  
   17.22  fun warn thm = warning ("InductiveCodegen: Not a proper clause:\n" ^
   17.23 @@ -653,7 +651,6 @@
   17.24  
   17.25  val setup =
   17.26    add_codegen "inductive" inductive_codegen #>
   17.27 -  CodegenData.init #>
   17.28    add_attribute "ind" (Scan.option (Args.$$$ "target" |-- Args.colon |-- Args.name) --
   17.29      Scan.option (Args.$$$ "params" |-- Args.colon |-- Args.nat) >> uncurry add);
   17.30  
    18.1 --- a/src/HOL/Tools/inductive_package.ML	Sun May 06 21:50:17 2007 +0200
    18.2 +++ b/src/HOL/Tools/inductive_package.ML	Mon May 07 00:49:59 2007 +0200
    18.3 @@ -86,7 +86,7 @@
    18.4  
    18.5  
    18.6  
    18.7 -(** theory data **)
    18.8 +(** context data **)
    18.9  
   18.10  type inductive_result =
   18.11    {preds: term list, defs: thm list, elims: thm list, raw_induct: thm,
   18.12 @@ -106,28 +106,25 @@
   18.13    {names: string list, coind: bool} * inductive_result;
   18.14  
   18.15  structure InductiveData = GenericDataFun
   18.16 -(struct
   18.17 -  val name = "HOL/inductive";
   18.18 +(
   18.19    type T = inductive_info Symtab.table * thm list;
   18.20 -
   18.21    val empty = (Symtab.empty, []);
   18.22    val extend = I;
   18.23    fun merge _ ((tab1, monos1), (tab2, monos2)) =
   18.24      (Symtab.merge (K true) (tab1, tab2), Drule.merge_rules (monos1, monos2));
   18.25 -
   18.26 -  fun print context (tab, monos) =
   18.27 -    let
   18.28 -      val ctxt = Context.proof_of context;
   18.29 -      val space = Consts.space_of (ProofContext.consts_of ctxt);
   18.30 -    in
   18.31 -      [Pretty.strs ("(co)inductives:" :: map #1 (NameSpace.extern_table (space, tab))),
   18.32 -       Pretty.big_list "monotonicity rules:" (map (ProofContext.pretty_thm ctxt) monos)]
   18.33 -      |> Pretty.chunks |> Pretty.writeln
   18.34 -    end;
   18.35 -end);
   18.36 +);
   18.37  
   18.38  val get_inductives = InductiveData.get o Context.Proof;
   18.39 -val print_inductives = InductiveData.print o Context.Proof;
   18.40 +
   18.41 +fun print_inductives ctxt =
   18.42 +  let
   18.43 +    val (tab, monos) = get_inductives ctxt;
   18.44 +    val space = Consts.space_of (ProofContext.consts_of ctxt);
   18.45 +  in
   18.46 +    [Pretty.strs ("(co)inductives:" :: map #1 (NameSpace.extern_table (space, tab))),
   18.47 +     Pretty.big_list "monotonicity rules:" (map (ProofContext.pretty_thm ctxt) monos)]
   18.48 +    |> Pretty.chunks |> Pretty.writeln
   18.49 +  end;
   18.50  
   18.51  
   18.52  (* get and put data *)
   18.53 @@ -156,7 +153,7 @@
   18.54            (_ $ (_ $ (Const ("Not", _) $ _) $ _)) => []
   18.55          | _ => [thm' RS (thm' RS eq_to_mono2)]);
   18.56      fun dest_less_concl thm = dest_less_concl (thm RS le_funD)
   18.57 -      handle THM _ => thm RS le_boolD      
   18.58 +      handle THM _ => thm RS le_boolD
   18.59    in
   18.60      case concl of
   18.61        Const ("==", _) $ _ $ _ => eq2mono (thm RS meta_eq_to_obj_eq)
   18.62 @@ -892,7 +889,6 @@
   18.63  (* setup theory *)
   18.64  
   18.65  val setup =
   18.66 -  InductiveData.init #>
   18.67    Method.add_methods [("ind_cases2", ind_cases,   (* FIXME "ind_cases" (?) *)
   18.68      "dynamic case analysis on predicates")] #>
   18.69    Attrib.add_attributes [("mono2", Attrib.add_del_args mono_add mono_del,   (* FIXME "mono" *)
    19.1 --- a/src/HOL/Tools/old_inductive_package.ML	Sun May 06 21:50:17 2007 +0200
    19.2 +++ b/src/HOL/Tools/old_inductive_package.ML	Mon May 07 00:49:59 2007 +0200
    19.3 @@ -37,7 +37,6 @@
    19.4      {defs: thm list, elims: thm list, raw_induct: thm, induct: thm,
    19.5       intrs: thm list, mk_cases: string -> thm, mono: thm, unfold: thm}) option
    19.6    val the_mk_cases: theory -> string -> string -> thm
    19.7 -  val print_inductives: theory -> unit
    19.8    val mono_add: attribute
    19.9    val mono_del: attribute
   19.10    val get_monos: theory -> thm list
   19.11 @@ -88,27 +87,14 @@
   19.12      induct: thm, intrs: thm list, mk_cases: string -> thm, mono: thm, unfold: thm};
   19.13  
   19.14  structure InductiveData = TheoryDataFun
   19.15 -(struct
   19.16 -  val name = "HOL/inductive";
   19.17 +(
   19.18    type T = inductive_info Symtab.table * thm list;
   19.19 -
   19.20    val empty = (Symtab.empty, []);
   19.21    val copy = I;
   19.22    val extend = I;
   19.23    fun merge _ ((tab1, monos1), (tab2, monos2)) =
   19.24      (Symtab.merge (K true) (tab1, tab2), Drule.merge_rules (monos1, monos2));
   19.25 -
   19.26 -  fun print thy (tab, monos) =
   19.27 -    [Pretty.strs ("(co)inductives:" ::
   19.28 -      map #1 (NameSpace.extern_table (Sign.const_space thy, tab))),
   19.29 -     Pretty.big_list "monotonicity rules:" (map (Display.pretty_thm_sg thy) monos)]
   19.30 -    |> Pretty.chunks |> Pretty.writeln;
   19.31 -end);
   19.32 -
   19.33 -val print_inductives = InductiveData.print;
   19.34 -
   19.35 -
   19.36 -(* get and put data *)
   19.37 +);
   19.38  
   19.39  val get_inductive = Symtab.lookup o #1 o InductiveData.get;
   19.40  
   19.41 @@ -871,7 +857,6 @@
   19.42  (* setup theory *)
   19.43  
   19.44  val setup =
   19.45 -  InductiveData.init #>
   19.46    Method.add_methods [("ind_cases", mk_cases_meth oo mk_cases_args,
   19.47      "dynamic case analysis on sets")] #>
   19.48    Attrib.add_attributes [("mono", Attrib.add_del_args mono_add mono_del,
    20.1 --- a/src/HOL/Tools/recdef_package.ML	Sun May 06 21:50:17 2007 +0200
    20.2 +++ b/src/HOL/Tools/recdef_package.ML	Mon May 07 00:49:59 2007 +0200
    20.3 @@ -8,7 +8,6 @@
    20.4  signature RECDEF_PACKAGE =
    20.5  sig
    20.6    val quiet_mode: bool ref
    20.7 -  val print_recdefs: theory -> unit
    20.8    val get_recdef: theory -> string
    20.9      -> {simps: thm list, rules: thm list list, induct: thm, tcs: term list} option
   20.10    val get_hints: Proof.context -> {simps: thm list, congs: (string * thm) list, wfs: thm list}
   20.11 @@ -97,10 +96,8 @@
   20.12  type recdef_info = {simps: thm list, rules: thm list list, induct: thm, tcs: term list};
   20.13  
   20.14  structure GlobalRecdefData = TheoryDataFun
   20.15 -(struct
   20.16 -  val name = "HOL/recdef";
   20.17 +(
   20.18    type T = recdef_info Symtab.table * hints;
   20.19 -
   20.20    val empty = (Symtab.empty, mk_hints ([], [], [])): T;
   20.21    val copy = I;
   20.22    val extend = I;
   20.23 @@ -111,14 +108,7 @@
   20.24          mk_hints (Drule.merge_rules (simps1, simps2),
   20.25            AList.merge (op =) Thm.eq_thm (congs1, congs2),
   20.26            Drule.merge_rules (wfs1, wfs2)));
   20.27 -
   20.28 -  fun print thy (tab, hints) =
   20.29 -    (Pretty.strs ("recdefs:" :: map #1 (NameSpace.extern_table (Sign.const_space thy, tab))) ::
   20.30 -      pretty_hints hints) |> Pretty.chunks |> Pretty.writeln;
   20.31 -end);
   20.32 -
   20.33 -val print_recdefs = GlobalRecdefData.print;
   20.34 -
   20.35 +);
   20.36  
   20.37  val get_recdef = Symtab.lookup o #1 o GlobalRecdefData.get;
   20.38  
   20.39 @@ -135,12 +125,10 @@
   20.40  (* proof data *)
   20.41  
   20.42  structure LocalRecdefData = ProofDataFun
   20.43 -(struct
   20.44 -  val name = "HOL/recdef";
   20.45 +(
   20.46    type T = hints;
   20.47    val init = get_global_hints;
   20.48 -  fun print _ hints = pretty_hints hints |> Pretty.chunks |> Pretty.writeln;
   20.49 -end);
   20.50 +);
   20.51  
   20.52  val get_hints = LocalRecdefData.get;
   20.53  fun map_hints f = Context.mapping (GlobalRecdefData.map (apsnd f)) (LocalRecdefData.map f);
   20.54 @@ -297,8 +285,6 @@
   20.55  (* setup theory *)
   20.56  
   20.57  val setup =
   20.58 -  GlobalRecdefData.init #>
   20.59 -  LocalRecdefData.init #>
   20.60    Attrib.add_attributes
   20.61     [(recdef_simpN, Attrib.add_del_args simp_add simp_del, "declaration of recdef simp rule"),
   20.62      (recdef_congN, Attrib.add_del_args cong_add cong_del, "declaration of recdef cong rule"),
    21.1 --- a/src/HOL/Tools/recfun_codegen.ML	Sun May 06 21:50:17 2007 +0200
    21.2 +++ b/src/HOL/Tools/recfun_codegen.ML	Mon May 07 00:49:59 2007 +0200
    21.3 @@ -18,15 +18,13 @@
    21.4  open Codegen;
    21.5  
    21.6  structure RecCodegenData = TheoryDataFun
    21.7 -(struct
    21.8 -  val name = "HOL/recfun_codegen";
    21.9 +(
   21.10    type T = (thm * string option) list Symtab.table;
   21.11    val empty = Symtab.empty;
   21.12    val copy = I;
   21.13    val extend = I;
   21.14    fun merge _ = Symtab.merge_list (Thm.eq_thm_prop o pairself fst);
   21.15 -  fun print _ _ = ();
   21.16 -end);
   21.17 +);
   21.18  
   21.19  
   21.20  val dest_eqn = HOLogic.dest_eq o HOLogic.dest_Trueprop;
   21.21 @@ -172,7 +170,6 @@
   21.22  
   21.23  
   21.24  val setup =
   21.25 -  RecCodegenData.init #>
   21.26    add_codegen "recfun" recfun_codegen #>
   21.27    add_attribute ""
   21.28      (Args.del |-- Scan.succeed del
    22.1 --- a/src/HOL/Tools/record_package.ML	Sun May 06 21:50:17 2007 +0200
    22.2 +++ b/src/HOL/Tools/record_package.ML	Mon May 07 00:49:59 2007 +0200
    22.3 @@ -243,7 +243,8 @@
    22.4  fun make_parent_info name fields extension induct =
    22.5   {name = name, fields = fields, extension = extension, induct = induct}: parent_info;
    22.6  
    22.7 -(* data kind 'HOL/record' *)
    22.8 +
    22.9 +(* theory data *)
   22.10  
   22.11  type record_data =
   22.12   {records: record_info Symtab.table,
   22.13 @@ -266,10 +267,8 @@
   22.14    extfields = extfields, fieldext = fieldext }: record_data;
   22.15  
   22.16  structure RecordsData = TheoryDataFun
   22.17 -(struct
   22.18 -  val name = "HOL/record"; 
   22.19 +(
   22.20    type T = record_data;
   22.21 -
   22.22    val empty =
   22.23      make_record_data Symtab.empty
   22.24        {selectors = Symtab.empty, updates = Symtab.empty, simpset = HOL_basic_ss}
   22.25 @@ -308,27 +307,26 @@
   22.26                      (splits1, splits2))
   22.27        (Symtab.merge (K true) (extfields1,extfields2))
   22.28        (Symtab.merge (K true) (fieldext1,fieldext2));
   22.29 +);
   22.30  
   22.31 -  fun print thy ({records = recs, ...}: record_data) =
   22.32 -    let
   22.33 -      val prt_typ = Sign.pretty_typ thy;
   22.34 -
   22.35 -      fun pretty_parent NONE = []
   22.36 -        | pretty_parent (SOME (Ts, name)) =
   22.37 -            [Pretty.block [prt_typ (Type (name, Ts)), Pretty.str " +"]];
   22.38 +fun print_records thy =
   22.39 +  let
   22.40 +    val {records = recs, ...} = RecordsData.get thy;
   22.41 +    val prt_typ = Sign.pretty_typ thy;
   22.42  
   22.43 -      fun pretty_field (c, T) = Pretty.block
   22.44 -        [Pretty.str (Sign.extern_const thy c), Pretty.str " ::",
   22.45 -          Pretty.brk 1, Pretty.quote (prt_typ T)];
   22.46 +    fun pretty_parent NONE = []
   22.47 +      | pretty_parent (SOME (Ts, name)) =
   22.48 +          [Pretty.block [prt_typ (Type (name, Ts)), Pretty.str " +"]];
   22.49  
   22.50 -      fun pretty_record (name, {args, parent, fields, ...}: record_info) =
   22.51 -        Pretty.block (Pretty.fbreaks (Pretty.block
   22.52 -          [prt_typ (Type (name, map TFree args)), Pretty.str " = "] ::
   22.53 -          pretty_parent parent @ map pretty_field fields));
   22.54 -    in map pretty_record (Symtab.dest recs) |> Pretty.chunks |> Pretty.writeln end;
   22.55 -end);
   22.56 +    fun pretty_field (c, T) = Pretty.block
   22.57 +      [Pretty.str (Sign.extern_const thy c), Pretty.str " ::",
   22.58 +        Pretty.brk 1, Pretty.quote (prt_typ T)];
   22.59  
   22.60 -val print_records = RecordsData.print;
   22.61 +    fun pretty_record (name, {args, parent, fields, ...}: record_info) =
   22.62 +      Pretty.block (Pretty.fbreaks (Pretty.block
   22.63 +        [prt_typ (Type (name, map TFree args)), Pretty.str " = "] ::
   22.64 +        pretty_parent parent @ map pretty_field fields));
   22.65 +  in map pretty_record (Symtab.dest recs) |> Pretty.chunks |> Pretty.writeln end;
   22.66  
   22.67  
   22.68  (* access 'records' *)
   22.69 @@ -343,6 +341,7 @@
   22.70        sel_upd equalities extinjects extsplit splits extfields fieldext;
   22.71    in RecordsData.put data thy end;
   22.72  
   22.73 +
   22.74  (* access 'sel_upd' *)
   22.75  
   22.76  val get_sel_upd = #sel_upd o RecordsData.get;
   22.77 @@ -365,6 +364,7 @@
   22.78         equalities extinjects extsplit splits extfields fieldext;
   22.79    in RecordsData.put data thy end;
   22.80  
   22.81 +
   22.82  (* access 'equalities' *)
   22.83  
   22.84  fun add_record_equalities name thm thy =
   22.85 @@ -378,18 +378,21 @@
   22.86  
   22.87  val get_equalities =Symtab.lookup o #equalities o RecordsData.get;
   22.88  
   22.89 +
   22.90  (* access 'extinjects' *)
   22.91  
   22.92  fun add_extinjects thm thy =
   22.93    let
   22.94      val {records, sel_upd, equalities, extinjects, extsplit, splits, extfields,fieldext} =
   22.95            RecordsData.get thy;
   22.96 -    val data = make_record_data records sel_upd equalities (insert Thm.eq_thm_prop thm extinjects) extsplit
   22.97 -                 splits extfields fieldext;
   22.98 +    val data =
   22.99 +      make_record_data records sel_upd equalities (insert Thm.eq_thm_prop thm extinjects) extsplit
  22.100 +        splits extfields fieldext;
  22.101    in RecordsData.put data thy end;
  22.102  
  22.103  val get_extinjects = rev o #extinjects o RecordsData.get;
  22.104  
  22.105 +
  22.106  (* access 'extsplit' *)
  22.107  
  22.108  fun add_extsplit name thm thy =
  22.109 @@ -2263,7 +2266,6 @@
  22.110  (* setup theory *)
  22.111  
  22.112  val setup =
  22.113 -  RecordsData.init #>
  22.114    Theory.add_trfuns ([], parse_translation, [], []) #>
  22.115    Theory.add_advanced_trfuns ([], adv_parse_translation, [], []) #>
  22.116    (fn thy => (Simplifier.change_simpset_of thy
    23.1 --- a/src/HOL/Tools/refute.ML	Sun May 06 21:50:17 2007 +0200
    23.2 +++ b/src/HOL/Tools/refute.ML	Mon May 07 00:49:59 2007 +0200
    23.3 @@ -186,9 +186,8 @@
    23.4      };
    23.5  
    23.6  
    23.7 -  structure RefuteDataArgs =
    23.8 -  struct
    23.9 -    val name = "HOL/refute";
   23.10 +  structure RefuteData = TheoryDataFun
   23.11 +  (
   23.12      type T =
   23.13        {interpreters: (string * (theory -> model -> arguments -> Term.term ->
   23.14          (interpretation * model * arguments) option)) list,
   23.15 @@ -204,15 +203,7 @@
   23.16        {interpreters = AList.merge (op =) (K true) (in1, in2),
   23.17         printers = AList.merge (op =) (K true) (pr1, pr2),
   23.18         parameters = Symtab.merge (op=) (pa1, pa2)};
   23.19 -    fun print sg {interpreters, printers, parameters} =
   23.20 -      Pretty.writeln (Pretty.chunks
   23.21 -        [Pretty.strs ("default parameters:" :: List.concat (map
   23.22 -          (fn (name, value) => [name, "=", value]) (Symtab.dest parameters))),
   23.23 -         Pretty.strs ("interpreters:" :: map fst interpreters),
   23.24 -         Pretty.strs ("printers:" :: map fst printers)]);
   23.25 -  end;
   23.26 -
   23.27 -  structure RefuteData = TheoryDataFun(RefuteDataArgs);
   23.28 +  );
   23.29  
   23.30  
   23.31  (* ------------------------------------------------------------------------- *)
   23.32 @@ -3210,7 +3201,6 @@
   23.33    (* (theory -> theory) list *)
   23.34  
   23.35    val setup =
   23.36 -     RefuteData.init #>
   23.37       add_interpreter "stlc"    stlc_interpreter #>
   23.38       add_interpreter "Pure"    Pure_interpreter #>
   23.39       add_interpreter "HOLogic" HOLogic_interpreter #>
    24.1 --- a/src/HOL/Tools/res_atpset.ML	Sun May 06 21:50:17 2007 +0200
    24.2 +++ b/src/HOL/Tools/res_atpset.ML	Mon May 07 00:49:59 2007 +0200
    24.3 @@ -18,24 +18,22 @@
    24.4  
    24.5  structure Data = GenericDataFun
    24.6  (
    24.7 -  val name = "HOL/atpset";
    24.8    type T = thm list;
    24.9    val empty = [];
   24.10    val extend = I;
   24.11    fun merge _ = Drule.merge_rules;
   24.12 -  fun print context rules =
   24.13 -    Pretty.writeln (Pretty.big_list "ATP rules:"
   24.14 -      (map (ProofContext.pretty_thm (Context.proof_of context)) rules));
   24.15  );
   24.16  
   24.17 -val print_atpset = Data.print o Context.Proof;
   24.18  val get_atpset = Data.get o Context.Proof;
   24.19  
   24.20 +fun print_atpset ctxt =
   24.21 +  Pretty.writeln (Pretty.big_list "ATP rules:"
   24.22 +    (map (ProofContext.pretty_thm ctxt) (get_atpset ctxt)));
   24.23 +
   24.24  val atp_add = Thm.declaration_attribute (Data.map o Drule.add_rule);
   24.25  val atp_del = Thm.declaration_attribute (Data.map o Drule.del_rule);
   24.26  
   24.27  val setup =
   24.28 -  Data.init #>
   24.29    Attrib.add_attributes [("atp", Attrib.add_del_args atp_add atp_del, "declaration of ATP rules")];
   24.30  
   24.31  end;
    25.1 --- a/src/HOL/Tools/res_axioms.ML	Sun May 06 21:50:17 2007 +0200
    25.2 +++ b/src/HOL/Tools/res_axioms.ML	Mon May 07 00:49:59 2007 +0200
    25.3 @@ -481,15 +481,13 @@
    25.4        (SOME (to_nnf th, fake_name th)  handle THM _ => NONE);
    25.5  
    25.6  structure ThmCache = TheoryDataFun
    25.7 -(struct
    25.8 -  val name = "ATP/thm_cache";
    25.9 +(
   25.10    type T = (thm list) Thmtab.table ref;
   25.11    val empty : T = ref Thmtab.empty;
   25.12    fun copy (ref tab) : T = ref tab;
   25.13    val extend = copy;
   25.14    fun merge _ (ref tab1, ref tab2) : T = ref (Thmtab.merge (K true) (tab1, tab2));
   25.15 -  fun print _ _ = ();
   25.16 -end);
   25.17 +);
   25.18  
   25.19  (*The cache prevents repeated clausification of a theorem, and also repeated declaration of 
   25.20    Skolem functions. The global one holds theorems proved prior to this point. Theory data
    26.1 --- a/src/HOL/Tools/typecopy_package.ML	Sun May 06 21:50:17 2007 +0200
    26.2 +++ b/src/HOL/Tools/typecopy_package.ML	Mon May 07 00:49:59 2007 +0200
    26.3 @@ -23,7 +23,7 @@
    26.4    val add_hook: hook -> theory -> theory
    26.5    val get_spec: theory -> string -> (string * sort) list * (string * typ list) list
    26.6    val get_eq: theory -> string -> thm
    26.7 -  val print: theory -> unit
    26.8 +  val print_typecopies: theory -> unit
    26.9    val setup: theory -> theory
   26.10  end;
   26.11  
   26.12 @@ -44,33 +44,30 @@
   26.13  type hook = string * info -> theory -> theory;
   26.14  
   26.15  structure TypecopyData = TheoryDataFun
   26.16 -(struct
   26.17 -  val name = "HOL/typecopy_package";
   26.18 +(
   26.19    type T = info Symtab.table * (serial * hook) list;
   26.20    val empty = (Symtab.empty, []);
   26.21    val copy = I;
   26.22    val extend = I;
   26.23    fun merge _ ((tab1, hooks1), (tab2, hooks2) : T) =
   26.24      (Symtab.merge (K true) (tab1, tab2), AList.merge (op =) (K true) (hooks1, hooks2));
   26.25 -  fun print thy (tab, _) =
   26.26 -    let
   26.27 -      fun mk (tyco, { vs, constr, typ, proj = (proj, _), ... } : info) =
   26.28 -        (Pretty.block o Pretty.breaks) [
   26.29 -          Sign.pretty_typ thy (Type (tyco, map TFree vs)),
   26.30 -          Pretty.str "=",
   26.31 -          (Pretty.str o Sign.extern_const thy) constr,
   26.32 -          Sign.pretty_typ thy typ,
   26.33 -          Pretty.block [Pretty.str "(", (Pretty.str o Sign.extern_const thy) proj, Pretty.str  ")"]
   26.34 -        ];
   26.35 +);
   26.36 +
   26.37 +fun print_typecopies thy =
   26.38 +  let
   26.39 +    val (tab, _) = TypecopyData.get thy;
   26.40 +    fun mk (tyco, { vs, constr, typ, proj = (proj, _), ... } : info) =
   26.41 +      (Pretty.block o Pretty.breaks) [
   26.42 +        Sign.pretty_typ thy (Type (tyco, map TFree vs)),
   26.43 +        Pretty.str "=",
   26.44 +        (Pretty.str o Sign.extern_const thy) constr,
   26.45 +        Sign.pretty_typ thy typ,
   26.46 +        Pretty.block [Pretty.str "(", (Pretty.str o Sign.extern_const thy) proj, Pretty.str  ")"]];
   26.47      in
   26.48 -      (Pretty.writeln o Pretty.block o Pretty.fbreaks) (
   26.49 -        Pretty.str "type copies:"
   26.50 -        :: map mk (Symtab.dest tab)
   26.51 -      )
   26.52 +      (Pretty.writeln o Pretty.block o Pretty.fbreaks)
   26.53 +        (Pretty.str "type copies:" :: map mk (Symtab.dest tab))
   26.54      end;
   26.55 -end);
   26.56  
   26.57 -val print = TypecopyData.print;
   26.58  val get_typecopies = Symtab.keys o fst o TypecopyData.get;
   26.59  val get_typecopy_info = Symtab.lookup o fst o TypecopyData.get;
   26.60  
   26.61 @@ -128,7 +125,7 @@
   26.62  
   26.63  val add_typecopy = gen_add_typecopy Sign.certify_typ;
   26.64  
   26.65 -end; (*local*)
   26.66 +end;
   26.67  
   26.68  
   26.69  (* equality function equation and datatype specification *)
   26.70 @@ -147,8 +144,6 @@
   26.71  fun add_project (_ , {proj_def, ...} : info) =
   26.72    CodegenData.add_func true proj_def;
   26.73  
   26.74 -val setup =
   26.75 -  TypecopyData.init
   26.76 -  #> add_hook add_project;
   26.77 +val setup = add_hook add_project;
   26.78  
   26.79 -end; (*struct*)
   26.80 +end;
    27.1 --- a/src/HOL/Tools/typedef_package.ML	Sun May 06 21:50:17 2007 +0200
    27.2 +++ b/src/HOL/Tools/typedef_package.ML	Mon May 07 00:49:59 2007 +0200
    27.3 @@ -24,7 +24,6 @@
    27.4      * (string * string) option -> theory -> Proof.state
    27.5    val typedef_i: (bool * string) * (bstring * string list * mixfix) * term
    27.6      * (string * string) option -> theory -> Proof.state
    27.7 -  val setup: theory -> theory
    27.8  end;
    27.9  
   27.10  structure TypedefPackage: TYPEDEF_PACKAGE =
   27.11 @@ -77,15 +76,13 @@
   27.12    Abs_cases: thm, Rep_induct: thm, Abs_induct: thm};
   27.13  
   27.14  structure TypedefData = TheoryDataFun
   27.15 -(struct
   27.16 -  val name = "HOL/typedef";
   27.17 +(
   27.18    type T = info Symtab.table;
   27.19    val empty = Symtab.empty;
   27.20    val copy = I;
   27.21    val extend = I;
   27.22    fun merge _ tabs : T = Symtab.merge (K true) tabs;
   27.23 -  fun print _ _ = ();
   27.24 -end);
   27.25 +);
   27.26  
   27.27  val get_info = Symtab.lookup o TypedefData.get;
   27.28  fun put_info name info = TypedefData.map (Symtab.update (name, info));
   27.29 @@ -270,8 +267,6 @@
   27.30  
   27.31  end;
   27.32  
   27.33 -val setup = TypedefData.init;
   27.34 -
   27.35  
   27.36  
   27.37  (** outer syntax **)
    28.1 --- a/src/HOL/Typedef.thy	Sun May 06 21:50:17 2007 +0200
    28.2 +++ b/src/HOL/Typedef.thy	Mon May 07 00:49:59 2007 +0200
    28.3 @@ -90,8 +90,7 @@
    28.4  use "Tools/typedef_codegen.ML"
    28.5  
    28.6  setup {*
    28.7 -  TypedefPackage.setup
    28.8 -  #> TypecopyPackage.setup
    28.9 +  TypecopyPackage.setup
   28.10    #> TypedefCodegen.setup
   28.11  *}
   28.12  
    29.1 --- a/src/HOL/arith_data.ML	Sun May 06 21:50:17 2007 +0200
    29.2 +++ b/src/HOL/arith_data.ML	Mon May 07 00:49:59 2007 +0200
    29.3 @@ -206,8 +206,7 @@
    29.4  fun eq_arith_tactic (ArithTactic {id = id1, ...}, ArithTactic {id = id2, ...}) = (id1 = id2);
    29.5  
    29.6  structure ArithTheoryData = TheoryDataFun
    29.7 -(struct
    29.8 -  val name = "HOL/arith";
    29.9 +(
   29.10    type T = {splits: thm list,
   29.11              inj_consts: (string * typ) list,
   29.12              discrete: string list,
   29.13 @@ -221,8 +220,7 @@
   29.14      inj_consts = Library.merge (op =) (inj_consts1, inj_consts2),
   29.15      discrete = Library.merge (op =) (discrete1, discrete2),
   29.16      tactics = Library.merge eq_arith_tactic (tactics1, tactics2)};
   29.17 -  fun print _ _ = ();
   29.18 -end);
   29.19 +);
   29.20  
   29.21  val arith_split_add = Thm.declaration_attribute (fn thm =>
   29.22    Context.mapping (ArithTheoryData.map (fn {splits,inj_consts,discrete,tactics} =>
   29.23 @@ -922,7 +920,6 @@
   29.24     Most of the work is done by the cancel tactics. *)
   29.25  
   29.26  val init_lin_arith_data =
   29.27 - Fast_Arith.setup #>
   29.28   Fast_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, ...} =>
   29.29     {add_mono_thms = add_mono_thms @
   29.30      @{thms add_mono_thms_ordered_semiring} @ @{thms add_mono_thms_ordered_field},
   29.31 @@ -940,7 +937,6 @@
   29.32        addsimprocs [ab_group_add_cancel.sum_conv, ab_group_add_cancel.rel_conv]
   29.33         (*abel_cancel helps it work in abstract algebraic domains*)
   29.34        addsimprocs nat_cancel_sums_add}) #>
   29.35 -  ArithTheoryData.init #>
   29.36    arith_discrete "nat";
   29.37  
   29.38  val fast_nat_arith_simproc =
    30.1 --- a/src/Provers/Arith/fast_lin_arith.ML	Sun May 06 21:50:17 2007 +0200
    30.2 +++ b/src/Provers/Arith/fast_lin_arith.ML	Mon May 07 00:49:59 2007 +0200
    30.3 @@ -86,7 +86,6 @@
    30.4  
    30.5  signature FAST_LIN_ARITH =
    30.6  sig
    30.7 -  val setup: theory -> theory
    30.8    val map_data: ({add_mono_thms: thm list, mult_mono_thms: thm list, inj_thms: thm list,
    30.9                   lessD: thm list, neqE: thm list, simpset: Simplifier.simpset}
   30.10                   -> {add_mono_thms: thm list, mult_mono_thms: thm list, inj_thms: thm list,
   30.11 @@ -99,18 +98,15 @@
   30.12    val cut_lin_arith_tac: simpset -> int -> tactic
   30.13  end;
   30.14  
   30.15 -functor Fast_Lin_Arith(structure LA_Logic:LIN_ARITH_LOGIC 
   30.16 +functor Fast_Lin_Arith(structure LA_Logic:LIN_ARITH_LOGIC
   30.17                         and       LA_Data:LIN_ARITH_DATA) : FAST_LIN_ARITH =
   30.18  struct
   30.19  
   30.20  
   30.21  (** theory data **)
   30.22  
   30.23 -(* data kind 'Provers/fast_lin_arith' *)
   30.24 -
   30.25  structure Data = TheoryDataFun
   30.26 -(struct
   30.27 -  val name = "Provers/fast_lin_arith";
   30.28 +(
   30.29    type T = {add_mono_thms: thm list, mult_mono_thms: thm list, inj_thms: thm list,
   30.30              lessD: thm list, neqE: thm list, simpset: Simplifier.simpset};
   30.31  
   30.32 @@ -130,12 +126,9 @@
   30.33       lessD = Drule.merge_rules (lessD1, lessD2),
   30.34       neqE = Drule.merge_rules (neqE1, neqE2),
   30.35       simpset = Simplifier.merge_ss (simpset1, simpset2)};
   30.36 -
   30.37 -  fun print _ _ = ();
   30.38 -end);
   30.39 +);
   30.40  
   30.41  val map_data = Data.map;
   30.42 -val setup = Data.init;
   30.43  
   30.44  
   30.45  
   30.46 @@ -424,7 +417,7 @@
   30.47  local
   30.48   exception FalseE of thm
   30.49  in
   30.50 -fun mkthm (sg:theory, ss:simpset) (asms:thm list) (just:injust) : thm =
   30.51 +fun mkthm (sg:theory, ss) (asms:thm list) (just:injust) : thm =
   30.52    let val {add_mono_thms, mult_mono_thms, inj_thms, lessD, simpset, ...} =
   30.53            Data.get sg;
   30.54        val simpset' = Simplifier.inherit_context ss simpset;
   30.55 @@ -503,7 +496,7 @@
   30.56  fun integ(rlhs,r,rel,rrhs,s,d) =
   30.57  let val (rn,rd) = Rat.quotient_of_rat r and (sn,sd) = Rat.quotient_of_rat s
   30.58      val m = lcms(map (abs o snd o Rat.quotient_of_rat) (r :: s :: map snd rlhs @ map snd rrhs))
   30.59 -    fun mult(t,r) = 
   30.60 +    fun mult(t,r) =
   30.61          let val (i,j) = Rat.quotient_of_rat r
   30.62          in (t,i * (m div j)) end
   30.63  in (m,(map mult rlhs, rn*(m div rd), rel, map mult rrhs, sn*(m div sd), d)) end
   30.64 @@ -527,7 +520,7 @@
   30.65                  else lineq(c,Lt,diff,just)
   30.66       | "~<"  => lineq(~c,Le,map (op~) diff,NotLessD(just))
   30.67       | "="   => lineq(c,Eq,diff,just)
   30.68 -     | _     => sys_error("mklineq" ^ rel)   
   30.69 +     | _     => sys_error("mklineq" ^ rel)
   30.70    end;
   30.71  
   30.72  (* ------------------------------------------------------------------------- *)
   30.73 @@ -590,15 +583,9 @@
   30.74  (*        failure as soon as a case could not be refuted; i.e. delay further *)
   30.75  (*        splitting until after a refutation for other cases has been found. *)
   30.76  
   30.77 -fun split_items sg (do_pre : bool) (Ts : typ list, terms : term list) :
   30.78 +fun split_items sg (do_pre : bool) (Ts, terms) :
   30.79                  (typ list * (LA_Data.decompT * int) list) list =
   30.80  let
   30.81 -(*
   30.82 -  val _ = if !trace then
   30.83 -            trace_msg ("split_items: Ts    = " ^ string_of_list (Sign.string_of_typ sg) Ts ^ "\n" ^
   30.84 -                       "             terms = " ^ string_of_list (Sign.string_of_term sg) terms)
   30.85 -          else ()
   30.86 -*)
   30.87    (* splits inequalities '~=' into '<' and '>'; this corresponds to *)
   30.88    (* 'REPEAT_DETERM (eresolve_tac neqE i)' at the theorem/tactic    *)
   30.89    (* level                                                          *)
   30.90 @@ -634,38 +621,14 @@
   30.91  
   30.92    val result = (Ts, terms)
   30.93      |> (* user-defined preprocessing of the subgoal *)
   30.94 -       (* (typ list * term list) list *)
   30.95         (if do_pre then LA_Data.pre_decomp sg else Library.single)
   30.96 -    |> (* compute the internal encoding of (in-)equalities *)
   30.97 -       (* (typ list * (LA_Data.decompT option * bool) list) list *)
   30.98 +    |> (* produce the internal encoding of (in-)equalities *)
   30.99         map (apsnd (map (fn t => (LA_Data.decomp sg t, LA_Data.domain_is_nat t))))
  30.100      |> (* splitting of inequalities *)
  30.101 -       (* (typ list * (LA_Data.decompT option * bool) list list) list *)
  30.102         map (apsnd elim_neq)
  30.103 -    |> (* combine the list of lists of subgoals into a single list *)
  30.104 -       map (fn (Ts, subgoals) => map (pair Ts o map fst) subgoals)
  30.105 -    |> List.concat
  30.106 +    |> maps (fn (Ts, subgoals) => map (pair Ts o map fst) subgoals)
  30.107      |> (* numbering of hypotheses, ignoring irrelevant ones *)
  30.108         map (apsnd (number_hyps 0))
  30.109 -(*
  30.110 -  val _ = if !trace then
  30.111 -            trace_msg ("split_items: result has " ^ Int.toString (length result) ^
  30.112 -              " subgoal(s)" ^ "\n" ^ (cat_lines o fst) (fold_map (fn (Ts, items) => fn n =>
  30.113 -                ("  " ^ Int.toString n ^ ". Ts    = " ^
  30.114 -                   string_of_list (Sign.string_of_typ sg) Ts ^ "\n" ^
  30.115 -                 "     items = " ^ string_of_list (string_of_pair 
  30.116 -                   (fn (l, i, rel, r, j, d) => enclose "(" ")" (commas
  30.117 -                     [string_of_list
  30.118 -                        (string_of_pair (Sign.string_of_term sg) Rat.string_of_rat) l,
  30.119 -                      Rat.string_of_rat i,
  30.120 -                      rel,
  30.121 -                      string_of_list
  30.122 -                        (string_of_pair (Sign.string_of_term sg) Rat.string_of_rat) r,
  30.123 -                      Rat.string_of_rat j,
  30.124 -                      Bool.toString d]))
  30.125 -                   Int.toString) items, n+1)) result 1))
  30.126 -          else ()
  30.127 -*)
  30.128  in result end;
  30.129  
  30.130  fun add_atoms (ats : term list, ((lhs,_,_,rhs,_,_) : LA_Data.decompT, _)) : term list =
  30.131 @@ -742,7 +705,7 @@
  30.132        refute sg params show_ex do_pre Hs'
  30.133    end;
  30.134  
  30.135 -fun refute_tac (ss : simpset) (i : int, justs : injust list) : tactic =
  30.136 +fun refute_tac ss (i, justs) =
  30.137    fn state =>
  30.138      let val _ = trace_thm ("refute_tac (on subgoal " ^ Int.toString i ^ ", with " ^
  30.139                               Int.toString (length justs) ^ " justification(s)):") state
    31.1 --- a/src/Provers/classical.ML	Sun May 06 21:50:17 2007 +0200
    31.2 +++ b/src/Provers/classical.ML	Mon May 07 00:49:59 2007 +0200
    31.3 @@ -140,9 +140,9 @@
    31.4    val add_context_unsafe_wrapper: string * (Proof.context -> wrapper) -> theory -> theory
    31.5    val del_context_unsafe_wrapper: string -> theory -> theory
    31.6    val get_claset: theory -> claset
    31.7 -  val print_local_claset: Proof.context -> unit
    31.8    val get_local_claset: Proof.context -> claset
    31.9    val put_local_claset: claset -> Proof.context -> Proof.context
   31.10 +  val print_local_claset: Proof.context -> unit
   31.11    val safe_dest: int option -> attribute
   31.12    val safe_elim: int option -> attribute
   31.13    val safe_intro: int option -> attribute
   31.14 @@ -857,19 +857,16 @@
   31.15  (* global claset *)
   31.16  
   31.17  structure GlobalClaset = TheoryDataFun
   31.18 -(struct
   31.19 -  val name = "Provers/claset";
   31.20 +(
   31.21    type T = claset ref * context_cs;
   31.22 -
   31.23    val empty = (ref empty_cs, empty_context_cs);
   31.24    fun copy (ref cs, ctxt_cs) = (ref cs, ctxt_cs): T;
   31.25    val extend = copy;
   31.26    fun merge _ ((ref cs1, ctxt_cs1), (ref cs2, ctxt_cs2)) =
   31.27      (ref (merge_cs (cs1, cs2)), merge_context_cs (ctxt_cs1, ctxt_cs2));
   31.28 -  fun print _ (ref cs, _) = print_cs cs;
   31.29 -end);
   31.30 +);
   31.31  
   31.32 -val print_claset = GlobalClaset.print;
   31.33 +val print_claset = print_cs o ! o #1 o GlobalClaset.get;
   31.34  val get_claset = ! o #1 o GlobalClaset.get;
   31.35  
   31.36  val get_context_cs = #2 o GlobalClaset.get o ProofContext.theory_of;
   31.37 @@ -912,20 +909,19 @@
   31.38  (* local claset *)
   31.39  
   31.40  structure LocalClaset = ProofDataFun
   31.41 -(struct
   31.42 -  val name = "Provers/claset";
   31.43 +(
   31.44    type T = claset;
   31.45    val init = get_claset;
   31.46 -  fun print ctxt cs = print_cs (context_cs ctxt cs (get_context_cs ctxt));
   31.47 -end);
   31.48 +);
   31.49  
   31.50 -val print_local_claset = LocalClaset.print;
   31.51  val get_local_claset = LocalClaset.get;
   31.52  val put_local_claset = LocalClaset.put;
   31.53  
   31.54  fun local_claset_of ctxt =
   31.55    context_cs ctxt (get_local_claset ctxt) (get_context_cs ctxt);
   31.56  
   31.57 +val print_local_claset = print_cs o local_claset_of;
   31.58 +
   31.59  
   31.60  (* attributes *)
   31.61  
   31.62 @@ -1061,7 +1057,7 @@
   31.63  
   31.64  (** theory setup **)
   31.65  
   31.66 -val setup = GlobalClaset.init #> LocalClaset.init #> setup_attrs #> setup_methods;
   31.67 +val setup = GlobalClaset.init #> setup_attrs #> setup_methods;
   31.68  
   31.69  
   31.70  
    32.1 --- a/src/Pure/Isar/attrib.ML	Sun May 06 21:50:17 2007 +0200
    32.2 +++ b/src/Pure/Isar/attrib.ML	Mon May 07 00:49:59 2007 +0200
    32.3 @@ -49,29 +49,24 @@
    32.4  (* theory data *)
    32.5  
    32.6  structure AttributesData = TheoryDataFun
    32.7 -(struct
    32.8 -  val name = "Isar/attributes";
    32.9 +(
   32.10    type T = (((src -> attribute) * string) * stamp) NameSpace.table;
   32.11 -
   32.12    val empty = NameSpace.empty_table;
   32.13    val copy = I;
   32.14    val extend = I;
   32.15 -
   32.16    fun merge _ tables = NameSpace.merge_tables (eq_snd (op =)) tables handle Symtab.DUPS dups =>
   32.17      error ("Attempt to merge different versions of attribute(s) " ^ commas_quote dups);
   32.18 +);
   32.19  
   32.20 -  fun print _ attribs =
   32.21 -    let
   32.22 -      fun prt_attr (name, ((_, comment), _)) = Pretty.block
   32.23 -        [Pretty.str (name ^ ":"), Pretty.brk 2, Pretty.str comment];
   32.24 -    in
   32.25 -      [Pretty.big_list "attributes:" (map prt_attr (NameSpace.extern_table attribs))]
   32.26 -      |> Pretty.chunks |> Pretty.writeln
   32.27 -    end;
   32.28 -end);
   32.29 -
   32.30 -val _ = Context.add_setup AttributesData.init;
   32.31 -val print_attributes = AttributesData.print;
   32.32 +fun print_attributes thy =
   32.33 +  let
   32.34 +    val attribs = AttributesData.get thy;
   32.35 +    fun prt_attr (name, ((_, comment), _)) = Pretty.block
   32.36 +      [Pretty.str (name ^ ":"), Pretty.brk 2, Pretty.str comment];
   32.37 +  in
   32.38 +    [Pretty.big_list "attributes:" (map prt_attr (NameSpace.extern_table attribs))]
   32.39 +    |> Pretty.chunks |> Pretty.writeln
   32.40 +  end;
   32.41  
   32.42  
   32.43  (* name space *)
    33.1 --- a/src/Pure/Isar/calculation.ML	Sun May 06 21:50:17 2007 +0200
    33.2 +++ b/src/Pure/Isar/calculation.ML	Mon May 07 00:49:59 2007 +0200
    33.3 @@ -30,25 +30,21 @@
    33.4  
    33.5  structure CalculationData = GenericDataFun
    33.6  (
    33.7 -  val name = "Isar/calculation";
    33.8    type T = (thm NetRules.T * thm list) * (thm list * int) option;
    33.9    val empty = ((NetRules.elim, []), NONE);
   33.10    val extend = I;
   33.11  
   33.12    fun merge _ (((trans1, sym1), _), ((trans2, sym2), _)) =
   33.13      ((NetRules.merge (trans1, trans2), Drule.merge_rules (sym1, sym2)), NONE);
   33.14 -
   33.15 -  fun print generic ((trans, sym), _) =
   33.16 -    let val ctxt = Context.proof_of generic in
   33.17 -      [Pretty.big_list "transitivity rules:"
   33.18 -          (map (ProofContext.pretty_thm ctxt) (NetRules.rules trans)),
   33.19 -        Pretty.big_list "symmetry rules:" (map (ProofContext.pretty_thm ctxt) sym)]
   33.20 -      |> Pretty.chunks |> Pretty.writeln
   33.21 -    end;
   33.22  );
   33.23  
   33.24 -val _ = Context.add_setup CalculationData.init;
   33.25 -val print_rules = CalculationData.print o Context.Proof;
   33.26 +fun print_rules ctxt =
   33.27 +  let val ((trans, sym), _) = CalculationData.get (Context.Proof ctxt) in
   33.28 +    [Pretty.big_list "transitivity rules:"
   33.29 +        (map (ProofContext.pretty_thm ctxt) (NetRules.rules trans)),
   33.30 +      Pretty.big_list "symmetry rules:" (map (ProofContext.pretty_thm ctxt) sym)]
   33.31 +    |> Pretty.chunks |> Pretty.writeln
   33.32 +  end;
   33.33  
   33.34  
   33.35  (* access calculation *)
    34.1 --- a/src/Pure/Isar/context_rules.ML	Sun May 06 21:50:17 2007 +0200
    34.2 +++ b/src/Pure/Isar/context_rules.ML	Mon May 07 00:49:59 2007 +0200
    34.3 @@ -94,9 +94,7 @@
    34.4  
    34.5  structure Rules = GenericDataFun
    34.6  (
    34.7 -  val name = "Pure/rules";
    34.8    type T = T;
    34.9 -
   34.10    val empty = make_rules ~1 [] empty_netpairs ([], []);
   34.11    val extend = I;
   34.12  
   34.13 @@ -112,20 +110,17 @@
   34.14            nth_map i (curry insert_tagged_brl ((w, n), (b, th))))
   34.15          (next upto ~1 ~~ rules) empty_netpairs;
   34.16      in make_rules (next - 1) rules netpairs wrappers end
   34.17 -
   34.18 -  fun print generic (Rules {rules, ...}) =
   34.19 -    let
   34.20 -      val ctxt = Context.proof_of generic;
   34.21 -      fun prt_kind (i, b) =
   34.22 -        Pretty.big_list ((the o AList.lookup (op =) kind_names) (i, b) ^ ":")
   34.23 -          (map_filter (fn (_, (k, th)) =>
   34.24 -              if k = (i, b) then SOME (ProofContext.pretty_thm ctxt th) else NONE)
   34.25 -            (sort (int_ord o pairself fst) rules));
   34.26 -    in Pretty.writeln (Pretty.chunks (map prt_kind rule_kinds)) end;
   34.27  );
   34.28  
   34.29 -val _ = Context.add_setup Rules.init;
   34.30 -val print_rules = Rules.print o Context.Proof;
   34.31 +fun print_rules ctxt =
   34.32 +  let
   34.33 +    val Rules {rules, ...} = Rules.get (Context.Proof ctxt);
   34.34 +    fun prt_kind (i, b) =
   34.35 +      Pretty.big_list ((the o AList.lookup (op =) kind_names) (i, b) ^ ":")
   34.36 +        (map_filter (fn (_, (k, th)) =>
   34.37 +            if k = (i, b) then SOME (ProofContext.pretty_thm ctxt th) else NONE)
   34.38 +          (sort (int_ord o pairself fst) rules));
   34.39 +  in Pretty.writeln (Pretty.chunks (map prt_kind rule_kinds)) end;
   34.40  
   34.41  
   34.42  (* access data *)
    35.1 --- a/src/Pure/Isar/induct_attrib.ML	Sun May 06 21:50:17 2007 +0200
    35.2 +++ b/src/Pure/Isar/induct_attrib.ML	Mon May 07 00:49:59 2007 +0200
    35.3 @@ -94,49 +94,43 @@
    35.4  
    35.5  (* context data *)
    35.6  
    35.7 -fun dest ((casesT, casesS), (inductT, inductS), (coinductT, coinductS)) =
    35.8 -  {type_cases = NetRules.rules casesT,
    35.9 -   set_cases = NetRules.rules casesS,
   35.10 -   type_induct = NetRules.rules inductT,
   35.11 -   set_induct = NetRules.rules inductS,
   35.12 -   type_coinduct = NetRules.rules coinductT,
   35.13 -   set_coinduct = NetRules.rules coinductS};
   35.14 -
   35.15  structure Induct = GenericDataFun
   35.16  (
   35.17 -  val name = "Isar/induct";
   35.18    type T = (rules * rules) * (rules * rules) * (rules * rules);
   35.19 -
   35.20    val empty =
   35.21      ((init_rules (left_var_prem o #2), init_rules (Thm.major_prem_of o #2)),
   35.22       (init_rules (right_var_concl o #2), init_rules (Thm.major_prem_of o #2)),
   35.23       (init_rules (left_var_concl o #2), init_rules (Thm.concl_of o #2)));
   35.24 -
   35.25    val extend = I;
   35.26 -
   35.27    fun merge _ (((casesT1, casesS1), (inductT1, inductS1), (coinductT1, coinductS1)),
   35.28        ((casesT2, casesS2), (inductT2, inductS2), (coinductT2, coinductS2))) =
   35.29      ((NetRules.merge (casesT1, casesT2), NetRules.merge (casesS1, casesS2)),
   35.30        (NetRules.merge (inductT1, inductT2), NetRules.merge (inductS1, inductS2)),
   35.31        (NetRules.merge (coinductT1, coinductT2), NetRules.merge (coinductS1, coinductS2)));
   35.32 -
   35.33 -  fun print generic ((casesT, casesS), (inductT, inductS), (coinductT, coinductS)) =
   35.34 -    let val ctxt = Context.proof_of generic in
   35.35 -     [pretty_rules ctxt "coinduct type:" coinductT,
   35.36 -      pretty_rules ctxt "coinduct set:" coinductS,
   35.37 -      pretty_rules ctxt "induct type:" inductT,
   35.38 -      pretty_rules ctxt "induct set:" inductS,
   35.39 -      pretty_rules ctxt "cases type:" casesT,
   35.40 -      pretty_rules ctxt "cases set:" casesS]
   35.41 -     |> Pretty.chunks |> Pretty.writeln
   35.42 -    end
   35.43  );
   35.44  
   35.45 -val _ = Context.add_setup Induct.init;
   35.46 -val print_rules = Induct.print o Context.Proof;
   35.47 -val dest_rules = dest o Induct.get o Context.Proof;
   35.48 +val get_local = Induct.get o Context.Proof;
   35.49  
   35.50 -val get_local = Induct.get o Context.Proof;
   35.51 +fun dest_rules ctxt =
   35.52 +  let val ((casesT, casesS), (inductT, inductS), (coinductT, coinductS)) = get_local ctxt in
   35.53 +    {type_cases = NetRules.rules casesT,
   35.54 +     set_cases = NetRules.rules casesS,
   35.55 +     type_induct = NetRules.rules inductT,
   35.56 +     set_induct = NetRules.rules inductS,
   35.57 +     type_coinduct = NetRules.rules coinductT,
   35.58 +     set_coinduct = NetRules.rules coinductS}
   35.59 +  end;
   35.60 +
   35.61 +fun print_rules ctxt =
   35.62 +  let val ((casesT, casesS), (inductT, inductS), (coinductT, coinductS)) = get_local ctxt in
   35.63 +   [pretty_rules ctxt "coinduct type:" coinductT,
   35.64 +    pretty_rules ctxt "coinduct set:" coinductS,
   35.65 +    pretty_rules ctxt "induct type:" inductT,
   35.66 +    pretty_rules ctxt "induct set:" inductS,
   35.67 +    pretty_rules ctxt "cases type:" casesT,
   35.68 +    pretty_rules ctxt "cases set:" casesS]
   35.69 +    |> Pretty.chunks |> Pretty.writeln
   35.70 +  end;
   35.71  
   35.72  
   35.73  (* access rules *)
    36.1 --- a/src/Pure/Isar/local_defs.ML	Sun May 06 21:50:17 2007 +0200
    36.2 +++ b/src/Pure/Isar/local_defs.ML	Mon May 07 00:49:59 2007 +0200
    36.3 @@ -147,19 +147,15 @@
    36.4  
    36.5  structure Rules = GenericDataFun
    36.6  (
    36.7 -  val name = "Pure/derived_defs";
    36.8    type T = thm list;
    36.9    val empty = []
   36.10    val extend = I;
   36.11    fun merge _ = Drule.merge_rules;
   36.12 -  fun print context rules =
   36.13 -    Pretty.writeln (Pretty.big_list "definitional transformations:"
   36.14 -      (map (ProofContext.pretty_thm (Context.proof_of context)) rules));
   36.15  );
   36.16  
   36.17 -val _ = Context.add_setup Rules.init;
   36.18 -
   36.19 -val print_rules = Rules.print o Context.Proof;
   36.20 +fun print_rules ctxt =
   36.21 +  Pretty.writeln (Pretty.big_list "definitional transformations:"
   36.22 +    (map (ProofContext.pretty_thm ctxt) (Rules.get (Context.Proof ctxt))));
   36.23  
   36.24  val defn_add = Thm.declaration_attribute (Rules.map o Drule.add_rule);
   36.25  val defn_del = Thm.declaration_attribute (Rules.map o Drule.del_rule);
    37.1 --- a/src/Pure/Isar/local_theory.ML	Sun May 06 21:50:17 2007 +0200
    37.2 +++ b/src/Pure/Isar/local_theory.ML	Mon May 07 00:49:59 2007 +0200
    37.3 @@ -88,12 +88,9 @@
    37.4  
    37.5  structure Data = ProofDataFun
    37.6  (
    37.7 -  val name = "Pure/local_theory";
    37.8    type T = lthy option;
    37.9    fun init _ = NONE;
   37.10 -  fun print _ _ = ();
   37.11  );
   37.12 -val _ = Context.add_setup Data.init;
   37.13  
   37.14  fun get_lthy lthy =
   37.15    (case Data.get lthy of
    38.1 --- a/src/Pure/Isar/locale.ML	Sun May 06 21:50:17 2007 +0200
    38.2 +++ b/src/Pure/Isar/locale.ML	Mon May 07 00:49:59 2007 +0200
    38.3 @@ -305,8 +305,7 @@
    38.4  (** theory data **)
    38.5  
    38.6  structure GlobalLocalesData = TheoryDataFun
    38.7 -(struct
    38.8 -  val name = "Isar/locales";
    38.9 +(
   38.10    type T = NameSpace.T * locale Symtab.table * Registrations.T Symtab.table;
   38.11      (* 1st entry: locale namespace,
   38.12         2nd entry: locales of the theory,
   38.13 @@ -332,33 +331,26 @@
   38.14    fun merge _ ((space1, locs1, regs1), (space2, locs2, regs2)) =
   38.15      (NameSpace.merge (space1, space2), Symtab.join join_locales (locs1, locs2),
   38.16       Symtab.join (K Registrations.join) (regs1, regs2));
   38.17 -
   38.18 -  fun print _ (space, locs, _) =
   38.19 -    Pretty.strs ("locales:" :: map #1 (NameSpace.extern_table (space, locs)))
   38.20 -    |> Pretty.writeln;
   38.21 -end);
   38.22 -
   38.23 -val _ = Context.add_setup GlobalLocalesData.init;
   38.24 +);
   38.25  
   38.26  
   38.27  
   38.28  (** context data **)
   38.29  
   38.30  structure LocalLocalesData = ProofDataFun
   38.31 -(struct
   38.32 -  val name = "Isar/locales";
   38.33 -  type T = Registrations.T Symtab.table;
   38.34 -    (* registrations, indexed by locale name *)
   38.35 +(
   38.36 +  type T = Registrations.T Symtab.table;  (*registrations, indexed by locale name*)
   38.37    fun init _ = Symtab.empty;
   38.38 -  fun print _ _ = ();
   38.39 -end);
   38.40 -
   38.41 -val _ = Context.add_setup LocalLocalesData.init;
   38.42 +);
   38.43  
   38.44  
   38.45  (* access locales *)
   38.46  
   38.47 -val print_locales = GlobalLocalesData.print;
   38.48 +fun print_locales thy =
   38.49 +  let val (space, locs, _) = GlobalLocalesData.get thy in
   38.50 +    Pretty.strs ("locales:" :: map #1 (NameSpace.extern_table (space, locs)))
   38.51 +    |> Pretty.writeln
   38.52 +  end;
   38.53  
   38.54  val intern = NameSpace.intern o #1 o GlobalLocalesData.get;
   38.55  val extern = NameSpace.extern o #1 o GlobalLocalesData.get;
    39.1 --- a/src/Pure/Isar/method.ML	Sun May 06 21:50:17 2007 +0200
    39.2 +++ b/src/Pure/Isar/method.ML	Mon May 07 00:49:59 2007 +0200
    39.3 @@ -378,28 +378,24 @@
    39.4  (* method definitions *)
    39.5  
    39.6  structure MethodsData = TheoryDataFun
    39.7 -(struct
    39.8 -  val name = "Isar/methods";
    39.9 +(
   39.10    type T = (((src -> Proof.context -> method) * string) * stamp) NameSpace.table;
   39.11 -
   39.12    val empty = NameSpace.empty_table;
   39.13    val copy = I;
   39.14    val extend = I;
   39.15    fun merge _ tables = NameSpace.merge_tables (eq_snd (op =)) tables handle Symtab.DUPS dups =>
   39.16      error ("Attempt to merge different versions of method(s) " ^ commas_quote dups);
   39.17 +);
   39.18  
   39.19 -  fun print _ meths =
   39.20 -    let
   39.21 -      fun prt_meth (name, ((_, comment), _)) = Pretty.block
   39.22 -        [Pretty.str (name ^ ":"), Pretty.brk 2, Pretty.str comment];
   39.23 -    in
   39.24 -      [Pretty.big_list "methods:" (map prt_meth (NameSpace.extern_table meths))]
   39.25 -      |> Pretty.chunks |> Pretty.writeln
   39.26 -    end;
   39.27 -end);
   39.28 -
   39.29 -val _ = Context.add_setup MethodsData.init;
   39.30 -val print_methods = MethodsData.print;
   39.31 +fun print_methods thy =
   39.32 +  let
   39.33 +    val meths = MethodsData.get thy;
   39.34 +    fun prt_meth (name, ((_, comment), _)) = Pretty.block
   39.35 +      [Pretty.str (name ^ ":"), Pretty.brk 2, Pretty.str comment];
   39.36 +  in
   39.37 +    [Pretty.big_list "methods:" (map prt_meth (NameSpace.extern_table meths))]
   39.38 +    |> Pretty.chunks |> Pretty.writeln
   39.39 +  end;
   39.40  
   39.41  
   39.42  (* get methods *)
    40.1 --- a/src/Pure/Isar/object_logic.ML	Sun May 06 21:50:17 2007 +0200
    40.2 +++ b/src/Pure/Isar/object_logic.ML	Mon May 07 00:49:59 2007 +0200
    40.3 @@ -38,11 +38,9 @@
    40.4  (** theory data **)
    40.5  
    40.6  structure ObjectLogicData = TheoryDataFun
    40.7 -(struct
    40.8 -  val name = "Pure/object_logic";
    40.9 +(
   40.10    type T = string option * (thm list * thm list);
   40.11 -
   40.12 -  val empty = (NONE, ([], [Drule.norm_hhf_eq]));
   40.13 +  val empty = (NONE, ([], []));
   40.14    val copy = I;
   40.15    val extend = I;
   40.16  
   40.17 @@ -53,11 +51,7 @@
   40.18    fun merge _ ((judgment1, (atomize1, rulify1)), (judgment2, (atomize2, rulify2))) =
   40.19      (merge_judgment (judgment1, judgment2),
   40.20        (Drule.merge_rules (atomize1, atomize2), Drule.merge_rules (rulify1, rulify2)));
   40.21 -
   40.22 -  fun print _ _ = ();
   40.23 -end);
   40.24 -
   40.25 -val _ = Context.add_setup ObjectLogicData.init;
   40.26 +);
   40.27  
   40.28  
   40.29  
   40.30 @@ -136,11 +130,13 @@
   40.31  val get_atomize = #1 o #2 o ObjectLogicData.get;
   40.32  val get_rulify = #2 o #2 o ObjectLogicData.get;
   40.33  
   40.34 -val declare_atomize = Thm.declaration_attribute (fn th =>
   40.35 -  Context.mapping (ObjectLogicData.map (apsnd (apfst (Drule.add_rule th)))) I);
   40.36 +val add_atomize = ObjectLogicData.map o apsnd o apfst o Drule.add_rule;
   40.37 +val add_rulify = ObjectLogicData.map o apsnd o apsnd o Drule.add_rule;
   40.38  
   40.39 -val declare_rulify = Thm.declaration_attribute (fn th =>
   40.40 -  Context.mapping (ObjectLogicData.map (apsnd (apsnd (Drule.add_rule th)))) I);
   40.41 +val declare_atomize = Thm.declaration_attribute (fn th => Context.mapping (add_atomize th) I);
   40.42 +val declare_rulify = Thm.declaration_attribute (fn th => Context.mapping (add_rulify th) I);
   40.43 +
   40.44 +val _ = Context.add_setup (add_rulify Drule.norm_hhf_eq);
   40.45  
   40.46  
   40.47  (* atomize *)
    41.1 --- a/src/Pure/Isar/proof_context.ML	Sun May 06 21:50:17 2007 +0200
    41.2 +++ b/src/Pure/Isar/proof_context.ML	Mon May 07 00:49:59 2007 +0200
    41.3 @@ -198,17 +198,13 @@
    41.4  
    41.5  structure ContextData = ProofDataFun
    41.6  (
    41.7 -  val name = "Isar/context";
    41.8    type T = ctxt;
    41.9    fun init thy =
   41.10      make_ctxt (false, local_naming, LocalSyntax.init thy,
   41.11        (Sign.consts_of thy, Sign.consts_of thy),
   41.12        (NameSpace.empty_table, FactIndex.empty), []);
   41.13 -  fun print _ _ = ();
   41.14  );
   41.15  
   41.16 -val _ = Context.add_setup ContextData.init;
   41.17 -
   41.18  fun rep_context ctxt = ContextData.get ctxt |> (fn Ctxt args => args);
   41.19  
   41.20  fun map_context f =
    42.1 --- a/src/Pure/Isar/theory_target.ML	Sun May 06 21:50:17 2007 +0200
    42.2 +++ b/src/Pure/Isar/theory_target.ML	Mon May 07 00:49:59 2007 +0200
    42.3 @@ -22,13 +22,10 @@
    42.4  
    42.5  structure Data = ProofDataFun
    42.6  (
    42.7 -  val name = "Isar/theory_target";
    42.8    type T = string option;
    42.9    fun init _ = NONE;
   42.10 -  fun print _ _ = ();
   42.11  );
   42.12  
   42.13 -val _ = Context.add_setup Data.init;
   42.14  val peek = Data.get;
   42.15  
   42.16  
    43.1 --- a/src/Pure/Proof/extraction.ML	Sun May 06 21:50:17 2007 +0200
    43.2 +++ b/src/Pure/Proof/extraction.ML	Mon May 07 00:49:59 2007 +0200
    43.3 @@ -171,11 +171,10 @@
    43.4  
    43.5  (**** theory data ****)
    43.6  
    43.7 -(* data kind 'Pure/extraction' *)
    43.8 +(* theory data *)
    43.9  
   43.10  structure ExtractionData = TheoryDataFun
   43.11 -(struct
   43.12 -  val name = "Pure/extraction";
   43.13 +(
   43.14    type T =
   43.15      {realizes_eqns : rules,
   43.16       typeof_eqns : rules,
   43.17 @@ -209,11 +208,7 @@
   43.18       defs = Library.merge Thm.eq_thm (defs1, defs2),
   43.19       expand = Library.merge (op =) (expand1, expand2),
   43.20       prep = (case prep1 of NONE => prep2 | _ => prep1)};
   43.21 -
   43.22 -  fun print _ _ = ();
   43.23 -end);
   43.24 -
   43.25 -val _ = Context.add_setup ExtractionData.init;
   43.26 +);
   43.27  
   43.28  fun read_condeq thy =
   43.29    let val thy' = add_syntax thy
    44.1 --- a/src/Pure/Thy/present.ML	Sun May 06 21:50:17 2007 +0200
    44.2 +++ b/src/Pure/Thy/present.ML	Mon May 07 00:49:59 2007 +0200
    44.3 @@ -75,17 +75,13 @@
    44.4  (** additional theory data **)
    44.5  
    44.6  structure BrowserInfoData = TheoryDataFun
    44.7 -(struct
    44.8 -  val name = "Pure/browser_info";
    44.9 +(
   44.10    type T = {name: string, session: string list, is_local: bool};
   44.11    val empty = {name = "", session = [], is_local = false}: T;
   44.12    val copy = I;
   44.13    fun extend _ = empty;
   44.14    fun merge _ _ = empty;
   44.15 -  fun print _ _ = ();
   44.16 -end);
   44.17 -
   44.18 -val _ = Context.add_setup BrowserInfoData.init;
   44.19 +);
   44.20  
   44.21  fun get_info thy =
   44.22    if member (op =) [Context.ProtoPureN, Context.PureN, Context.CPureN] (Context.theory_name thy)
    45.1 --- a/src/Pure/Thy/term_style.ML	Sun May 06 21:50:17 2007 +0200
    45.2 +++ b/src/Pure/Thy/term_style.ML	Mon May 07 00:49:59 2007 +0200
    45.3 @@ -22,19 +22,17 @@
    45.4    error ("Duplicate declaration of antiquote style(s): " ^ commas_quote names);
    45.5  
    45.6  structure StyleData = TheoryDataFun
    45.7 -(struct
    45.8 -  val name = "Isar/antiquote_style";
    45.9 +(
   45.10    type T = ((Proof.context -> term -> term) * stamp) Symtab.table;
   45.11    val empty = Symtab.empty;
   45.12    val copy = I;
   45.13    val extend = I;
   45.14    fun merge _ tabs = Symtab.merge (eq_snd (op =)) tabs
   45.15      handle Symtab.DUPS dups => err_dup_styles dups;
   45.16 -  fun print _ tab = Pretty.writeln (Pretty.strs ("antiquote styles:" :: Symtab.keys tab));
   45.17 -end);
   45.18 +);
   45.19  
   45.20 -val _ = Context.add_setup StyleData.init;
   45.21 -val print_styles = StyleData.print;
   45.22 +fun print_styles thy =
   45.23 +  Pretty.writeln (Pretty.strs ("antiquote styles:" :: Symtab.keys (StyleData.get thy)));
   45.24  
   45.25  
   45.26  (* accessors *)
    46.1 --- a/src/Pure/Tools/class_package.ML	Sun May 06 21:50:17 2007 +0200
    46.2 +++ b/src/Pure/Tools/class_package.ML	Mon May 07 00:49:59 2007 +0200
    46.3 @@ -237,20 +237,15 @@
    46.4  
    46.5  fun merge_pair f1 f2 ((x1, y1), (x2, y2)) = (f1 (x1, x2), f2 (y1, y2));
    46.6  
    46.7 -structure ClassData = TheoryDataFun (
    46.8 -  struct
    46.9 -    val name = "Pure/classes";
   46.10 -    type T = class_data Graph.T * class Symtab.table (*locale name ~> class name*);
   46.11 -    val empty = (Graph.empty, Symtab.empty);
   46.12 -    val copy = I;
   46.13 -    val extend = I;
   46.14 -    fun merge _ = merge_pair (Graph.merge (K true)) (Symtab.merge (K true));
   46.15 -    fun print _ _ = ();
   46.16 -  end
   46.17 +structure ClassData = TheoryDataFun
   46.18 +(
   46.19 +  type T = class_data Graph.T * class Symtab.table (*locale name ~> class name*);
   46.20 +  val empty = (Graph.empty, Symtab.empty);
   46.21 +  val copy = I;
   46.22 +  val extend = I;
   46.23 +  fun merge _ = merge_pair (Graph.merge (K true)) (Symtab.merge (K true));
   46.24  );
   46.25  
   46.26 -val _ = Context.add_setup ClassData.init;
   46.27 -
   46.28  
   46.29  (* queries *)
   46.30  
    47.1 --- a/src/Pure/Tools/codegen_data.ML	Sun May 06 21:50:17 2007 +0200
    47.2 +++ b/src/Pure/Tools/codegen_data.ML	Mon May 07 00:49:59 2007 +0200
    47.3 @@ -312,8 +312,7 @@
    47.4  type data = Object.T Datatab.table;
    47.5  
    47.6  structure CodeData = TheoryDataFun
    47.7 -(struct
    47.8 -  val name = "Pure/codegen_data";
    47.9 +(
   47.10    type T = exec * data ref;
   47.11    val empty = (empty_exec, ref Datatab.empty : data ref);
   47.12    fun copy (exec, data) = (exec, ref (! data));
   47.13 @@ -325,67 +324,67 @@
   47.14        val data2' = Datatab.map' (invoke_purge NONE touched) (! data2);
   47.15        val data = Datatab.join (invoke_merge pp) (data1', data2');
   47.16      in (exec, ref data) end;
   47.17 -  fun print thy (exec, _) =
   47.18 -    let
   47.19 -      val ctxt = ProofContext.init thy;
   47.20 -      fun pretty_func (s, lthms) =
   47.21 -        (Pretty.block o Pretty.fbreaks) (
   47.22 -          Pretty.str s :: pretty_sdthms ctxt lthms
   47.23 -        );
   47.24 -      fun pretty_dtyp (s, []) =
   47.25 +);
   47.26 +
   47.27 +fun print_codesetup thy =
   47.28 +  let
   47.29 +    val ctxt = ProofContext.init thy;
   47.30 +    val (exec, _) = CodeData.get thy;
   47.31 +    fun pretty_func (s, lthms) =
   47.32 +      (Pretty.block o Pretty.fbreaks) (
   47.33 +        Pretty.str s :: pretty_sdthms ctxt lthms
   47.34 +      );
   47.35 +    fun pretty_dtyp (s, []) =
   47.36 +          Pretty.str s
   47.37 +      | pretty_dtyp (s, cos) =
   47.38 +          (Pretty.block o Pretty.breaks) (
   47.39              Pretty.str s
   47.40 -        | pretty_dtyp (s, cos) =
   47.41 -            (Pretty.block o Pretty.breaks) (
   47.42 -              Pretty.str s
   47.43 -              :: Pretty.str "="
   47.44 -              :: separate (Pretty.str "|") (map (fn (c, []) => Pretty.str c
   47.45 -                   | (c, tys) =>
   47.46 -                       (Pretty.block o Pretty.breaks)
   47.47 -                          (Pretty.str c :: Pretty.str "of" :: map (Pretty.quote o Sign.pretty_typ thy) tys)) cos)
   47.48 -            );
   47.49 -      val inlines = (#inlines o the_preproc) exec;
   47.50 -      val inline_procs = (map fst o #inline_procs o the_preproc) exec;
   47.51 -      val preprocs = (map fst o #preprocs o the_preproc) exec;
   47.52 -      val funs = the_funcs exec
   47.53 -        |> Consttab.dest
   47.54 -        |> (map o apfst) (CodegenConsts.string_of_const thy)
   47.55 -        |> sort (string_ord o pairself fst);
   47.56 -      val dtyps = the_dtyps exec
   47.57 -        |> Symtab.dest
   47.58 -        |> map (fn (dtco, (vs, cos)) => (Sign.string_of_typ thy (Type (dtco, map TFree vs)), cos))
   47.59 -        |> sort (string_ord o pairself fst)
   47.60 -    in
   47.61 -      (Pretty.writeln o Pretty.chunks) [
   47.62 -        Pretty.block (
   47.63 -          Pretty.str "defining equations:"
   47.64 -          :: Pretty.fbrk
   47.65 -          :: (Pretty.fbreaks o map pretty_func) funs
   47.66 -        ),
   47.67 -        Pretty.block (
   47.68 -          Pretty.str "inlining theorems:"
   47.69 -          :: Pretty.fbrk
   47.70 -          :: (Pretty.fbreaks o map (ProofContext.pretty_thm ctxt)) inlines
   47.71 -        ),
   47.72 -        Pretty.block (
   47.73 -          Pretty.str "inlining procedures:"
   47.74 -          :: Pretty.fbrk
   47.75 -          :: (Pretty.fbreaks o map Pretty.str) inline_procs
   47.76 -        ),
   47.77 -        Pretty.block (
   47.78 -          Pretty.str "preprocessors:"
   47.79 -          :: Pretty.fbrk
   47.80 -          :: (Pretty.fbreaks o map Pretty.str) preprocs
   47.81 -        ),
   47.82 -        Pretty.block (
   47.83 -          Pretty.str "datatypes:"
   47.84 -          :: Pretty.fbrk
   47.85 -          :: (Pretty.fbreaks o map pretty_dtyp) dtyps
   47.86 -        )
   47.87 -      ]
   47.88 -    end;
   47.89 -end);
   47.90 -
   47.91 -val print_codesetup = CodeData.print;
   47.92 +            :: Pretty.str "="
   47.93 +            :: separate (Pretty.str "|") (map (fn (c, []) => Pretty.str c
   47.94 +                 | (c, tys) =>
   47.95 +                     (Pretty.block o Pretty.breaks)
   47.96 +                        (Pretty.str c :: Pretty.str "of" :: map (Pretty.quote o Sign.pretty_typ thy) tys)) cos)
   47.97 +          );
   47.98 +    val inlines = (#inlines o the_preproc) exec;
   47.99 +    val inline_procs = (map fst o #inline_procs o the_preproc) exec;
  47.100 +    val preprocs = (map fst o #preprocs o the_preproc) exec;
  47.101 +    val funs = the_funcs exec
  47.102 +      |> Consttab.dest
  47.103 +      |> (map o apfst) (CodegenConsts.string_of_const thy)
  47.104 +      |> sort (string_ord o pairself fst);
  47.105 +    val dtyps = the_dtyps exec
  47.106 +      |> Symtab.dest
  47.107 +      |> map (fn (dtco, (vs, cos)) => (Sign.string_of_typ thy (Type (dtco, map TFree vs)), cos))
  47.108 +      |> sort (string_ord o pairself fst)
  47.109 +  in
  47.110 +    (Pretty.writeln o Pretty.chunks) [
  47.111 +      Pretty.block (
  47.112 +        Pretty.str "defining equations:"
  47.113 +        :: Pretty.fbrk
  47.114 +        :: (Pretty.fbreaks o map pretty_func) funs
  47.115 +      ),
  47.116 +      Pretty.block (
  47.117 +        Pretty.str "inlining theorems:"
  47.118 +        :: Pretty.fbrk
  47.119 +        :: (Pretty.fbreaks o map (ProofContext.pretty_thm ctxt)) inlines
  47.120 +      ),
  47.121 +      Pretty.block (
  47.122 +        Pretty.str "inlining procedures:"
  47.123 +        :: Pretty.fbrk
  47.124 +        :: (Pretty.fbreaks o map Pretty.str) inline_procs
  47.125 +      ),
  47.126 +      Pretty.block (
  47.127 +        Pretty.str "preprocessors:"
  47.128 +        :: Pretty.fbrk
  47.129 +        :: (Pretty.fbreaks o map Pretty.str) preprocs
  47.130 +      ),
  47.131 +      Pretty.block (
  47.132 +        Pretty.str "datatypes:"
  47.133 +        :: Pretty.fbrk
  47.134 +        :: (Pretty.fbreaks o map pretty_dtyp) dtyps
  47.135 +      )
  47.136 +    ]
  47.137 +  end;
  47.138  
  47.139  fun init k = CodeData.map
  47.140    (fn (exec, data) => (exec, ref (Datatab.update (k, invoke_empty k) (! data))));
    48.1 --- a/src/Pure/Tools/codegen_names.ML	Sun May 06 21:50:17 2007 +0200
    48.2 +++ b/src/Pure/Tools/codegen_names.ML	Mon May 07 00:49:59 2007 +0200
    48.3 @@ -292,18 +292,16 @@
    48.4  end; (*local*)
    48.5  
    48.6  structure CodeName = TheoryDataFun
    48.7 -(struct
    48.8 -  val name = "Pure/codegen_names";
    48.9 +(
   48.10    type T = names ref;
   48.11    val empty = ref empty_names;
   48.12    fun copy (ref names) = ref names;
   48.13    val extend = copy;
   48.14    fun merge _ (ref names1, ref names2) = ref (merge_names (names1, names2));
   48.15 -  fun print _ _ = ();
   48.16 -end);
   48.17 +);
   48.18  
   48.19  structure ConstName = CodeDataFun
   48.20 -(struct
   48.21 +(
   48.22    val name = "Pure/codegen_names";
   48.23    type T = const Consttab.table * (string * string option) Symtab.table;
   48.24    val empty = (Consttab.empty, Symtab.empty);
   48.25 @@ -313,7 +311,7 @@
   48.26    fun purge _ NONE _ = empty
   48.27      | purge _ (SOME cs) (const, constrev) = (fold Consttab.delete_safe cs const,
   48.28          fold Symtab.delete (map_filter (Consttab.lookup const) cs) constrev);
   48.29 -end);
   48.30 +);
   48.31  
   48.32  val _ = Context.add_setup (CodeName.init #> ConstName.init);
   48.33  
    49.1 --- a/src/Pure/Tools/codegen_package.ML	Sun May 06 21:50:17 2007 +0200
    49.2 +++ b/src/Pure/Tools/codegen_package.ML	Mon May 07 00:49:59 2007 +0200
    49.3 @@ -51,18 +51,17 @@
    49.4      Consttab.merge CodegenConsts.eq_const (consts1, consts2));
    49.5  
    49.6  structure CodegenPackageData = TheoryDataFun
    49.7 -(struct
    49.8 -  val name = "Pure/codegen_package_setup";
    49.9 +(
   49.10    type T = appgens * abstypes;
   49.11    val empty = (Symtab.empty, (Symtab.empty, Consttab.empty));
   49.12    val copy = I;
   49.13    val extend = I;
   49.14    fun merge _ ((appgens1, abstypes1), (appgens2, abstypes2)) =
   49.15      (merge_appgens (appgens1, appgens2), merge_abstypes (abstypes1, abstypes2));
   49.16 -  fun print _ _ = ();
   49.17 -end);
   49.18 +);
   49.19  
   49.20 -structure Funcgr = CodegenFuncgrRetrieval (
   49.21 +structure Funcgr = CodegenFuncgrRetrieval
   49.22 +(
   49.23    val name = "Pure/codegen_package_thms";
   49.24    fun rewrites thy = [];
   49.25  );
   49.26 @@ -94,7 +93,7 @@
   49.27    in Present.display_graph prgr end;
   49.28  
   49.29  structure Code = CodeDataFun
   49.30 -(struct
   49.31 +(
   49.32    val name = "Pure/codegen_package_code";
   49.33    type T = CodegenThingol.code;
   49.34    val empty = CodegenThingol.empty_code;
   49.35 @@ -110,9 +109,9 @@
   49.36                o filter (member CodegenConsts.eq_const cs_exisiting)
   49.37              ) cs;
   49.38          in Graph.del_nodes dels code end;
   49.39 -end);
   49.40 +);
   49.41  
   49.42 -val _ = Context.add_setup (CodegenPackageData.init #> Funcgr.init #> Code.init);
   49.43 +val _ = Context.add_setup (Funcgr.init #> Code.init);
   49.44  
   49.45  
   49.46  (* preparing defining equations *)
    50.1 --- a/src/Pure/Tools/codegen_serializer.ML	Sun May 06 21:50:17 2007 +0200
    50.2 +++ b/src/Pure/Tools/codegen_serializer.ML	Mon May 07 00:49:59 2007 +0200
    50.3 @@ -1539,15 +1539,13 @@
    50.4      error ("Incompatible serializers: " ^ quote target);
    50.5  
    50.6  structure CodegenSerializerData = TheoryDataFun
    50.7 -(struct
    50.8 -  val name = "Pure/codegen_serializer";
    50.9 +(
   50.10    type T = target Symtab.table;
   50.11    val empty = Symtab.empty;
   50.12    val copy = I;
   50.13    val extend = I;
   50.14    fun merge _ = Symtab.join merge_target;
   50.15 -  fun print _ _ = ();
   50.16 -end);
   50.17 +);
   50.18  
   50.19  fun the_serializer (Target { serializer, ... }) = serializer;
   50.20  fun the_reserved (Target { reserved, ... }) = reserved;
   50.21 @@ -1587,8 +1585,7 @@
   50.22  val target_diag = "diag";
   50.23  
   50.24  val _ = Context.add_setup (
   50.25 -  CodegenSerializerData.init
   50.26 -  #> add_serializer (target_SML, isar_seri_sml)
   50.27 +  add_serializer (target_SML, isar_seri_sml)
   50.28    #> add_serializer (target_OCaml, isar_seri_ocaml)
   50.29    #> add_serializer (target_Haskell, isar_seri_haskell)
   50.30    #> add_serializer (target_diag, (fn _ => fn _ => fn _ => seri_diagnosis))
    51.1 --- a/src/Pure/Tools/nbe.ML	Sun May 06 21:50:17 2007 +0200
    51.2 +++ b/src/Pure/Tools/nbe.ML	Mon May 07 00:49:59 2007 +0200
    51.3 @@ -26,19 +26,14 @@
    51.4  (* preproc and postproc attributes *)
    51.5  
    51.6  structure NBE_Rewrite = TheoryDataFun
    51.7 -(struct
    51.8 -  val name = "Pure/nbe";
    51.9 +(
   51.10    type T = thm list * thm list
   51.11 -
   51.12 -  val empty = ([],[])
   51.13 +  val empty = ([], []);
   51.14    val copy = I;
   51.15    val extend = I;
   51.16 -
   51.17    fun merge _ ((pres1,posts1), (pres2,posts2)) =
   51.18      (Library.merge Thm.eq_thm (pres1,pres2), Library.merge Thm.eq_thm (posts1,posts2))
   51.19 -
   51.20 -  fun print _ _ = ()
   51.21 -end);
   51.22 +);
   51.23  
   51.24  val _ =
   51.25    let
   51.26 @@ -51,8 +46,7 @@
   51.27        || Args.$$$ "post" >> K attr_post));
   51.28    in
   51.29      Context.add_setup (
   51.30 -      NBE_Rewrite.init
   51.31 -      #> Attrib.add_attributes
   51.32 +      Attrib.add_attributes
   51.33            [("normal", attr, "declare rewrite theorems for normalization")]
   51.34      )
   51.35    end;
    52.1 --- a/src/Pure/assumption.ML	Sun May 06 21:50:17 2007 +0200
    52.2 +++ b/src/Pure/assumption.ML	Mon May 07 00:49:59 2007 +0200
    52.3 @@ -62,14 +62,10 @@
    52.4  
    52.5  structure Data = ProofDataFun
    52.6  (
    52.7 -  val name = "Pure/assumption";
    52.8    type T = data;
    52.9    fun init _ = make_data ([], []);
   52.10 -  fun print _ _ = ();
   52.11  );
   52.12  
   52.13 -val _ = Context.add_setup Data.init;
   52.14 -
   52.15  fun map_data f = Data.map (fn Data {assms, prems} => make_data (f (assms, prems)));
   52.16  fun rep_data ctxt = Data.get ctxt |> (fn Data args => args);
   52.17  
    53.1 --- a/src/Pure/axclass.ML	Sun May 06 21:50:17 2007 +0200
    53.2 +++ b/src/Pure/axclass.ML	Mon May 07 00:49:59 2007 +0200
    53.3 @@ -95,18 +95,14 @@
    53.4  (* setup data *)
    53.5  
    53.6  structure AxClassData = TheoryDataFun
    53.7 -(struct
    53.8 -  val name = "Pure/axclass";
    53.9 +(
   53.10    type T = axclasses * instances;
   53.11 -  val empty : T = ((Symtab.empty, []), ([], Symtab.empty));
   53.12 +  val empty = ((Symtab.empty, []), ([], Symtab.empty));
   53.13    val copy = I;
   53.14    val extend = I;
   53.15    fun merge pp ((axclasses1, instances1), (axclasses2, instances2)) =
   53.16      (merge_axclasses pp (axclasses1, axclasses2), (merge_instances (instances1, instances2)));
   53.17 -  fun print _ _ = ();
   53.18 -end);
   53.19 -
   53.20 -val _ = Context.add_setup AxClassData.init;
   53.21 +);
   53.22  
   53.23  
   53.24  (* maintain axclasses *)
    54.1 --- a/src/Pure/codegen.ML	Sun May 06 21:50:17 2007 +0200
    54.2 +++ b/src/Pure/codegen.ML	Mon May 07 00:49:59 2007 +0200
    54.3 @@ -199,13 +199,13 @@
    54.4    {size = size, iterations = iterations,
    54.5     default_type = SOME (Sign.read_typ thy s)};
    54.6  
    54.7 -(* data kind 'Pure/codegen' *)
    54.8 +
    54.9 +(* theory data *)
   54.10  
   54.11  structure CodeData = CodegenData;
   54.12  
   54.13  structure CodegenData = TheoryDataFun
   54.14 -(struct
   54.15 -  val name = "Pure/codegen";
   54.16 +(
   54.17    type T =
   54.18      {codegens : (string * term codegen) list,
   54.19       tycodegens : (string * typ codegen) list,
   54.20 @@ -237,15 +237,15 @@
   54.21       preprocs = AList.merge (op =) (K true) (preprocs1, preprocs2),
   54.22       modules = Symtab.merge (K true) (modules1, modules2),
   54.23       test_params = merge_test_params test_params1 test_params2};
   54.24 +);
   54.25  
   54.26 -  fun print _ ({codegens, tycodegens, ...} : T) =
   54.27 +fun print_codegens thy =
   54.28 +  let val {codegens, tycodegens, ...} = CodegenData.get thy in
   54.29      Pretty.writeln (Pretty.chunks
   54.30        [Pretty.strs ("term code generators:" :: map fst codegens),
   54.31 -       Pretty.strs ("type code generators:" :: map fst tycodegens)]);
   54.32 -end);
   54.33 +       Pretty.strs ("type code generators:" :: map fst tycodegens)])
   54.34 +  end;
   54.35  
   54.36 -val _ = Context.add_setup CodegenData.init;
   54.37 -val print_codegens = CodegenData.print;
   54.38  
   54.39  
   54.40  (**** access parameters for random testing ****)
    55.1 --- a/src/Pure/compress.ML	Sun May 06 21:50:17 2007 +0200
    55.2 +++ b/src/Pure/compress.ML	Mon May 07 00:49:59 2007 +0200
    55.3 @@ -21,8 +21,7 @@
    55.4  (* theory data *)
    55.5  
    55.6  structure CompressData = TheoryDataFun
    55.7 -(struct
    55.8 -  val name = "Pure/compress";
    55.9 +(
   55.10    type T = typ Typtab.table ref * term Termtab.table ref;
   55.11    val empty : T = (ref Typtab.empty, ref Termtab.empty);
   55.12    fun copy (ref typs, ref terms) : T = (ref typs, ref terms);
   55.13 @@ -30,8 +29,7 @@
   55.14    fun merge _ ((ref typs1, ref terms1), (ref typs2, ref terms2)) : T =
   55.15     (ref (Typtab.merge (K true) (typs1, typs2)),
   55.16      ref (Termtab.merge (K true) (terms1, terms2)));
   55.17 -  fun print _ _ = ();
   55.18 -end);
   55.19 +);
   55.20  
   55.21  val init_data = CompressData.init;
   55.22  
    56.1 --- a/src/Pure/display.ML	Sun May 06 21:50:17 2007 +0200
    56.2 +++ b/src/Pure/display.ML	Mon May 07 00:49:59 2007 +0200
    56.3 @@ -234,9 +234,6 @@
    56.4      val rests = restricts |> map (apfst (apfst extern_const)) |> sort_wrt (#1 o #1);
    56.5    in
    56.6      [Pretty.strs ("names:" :: Context.names_of thy)] @
    56.7 -    (if verbose then
    56.8 -      [Pretty.strs ("theory data:" :: Context.theory_data_of thy),
    56.9 -       Pretty.strs ("proof data:" :: Context.proof_data_of thy)] else []) @
   56.10      [Pretty.strs ["name prefix:", NameSpace.path_of naming],
   56.11        Pretty.big_list "classes:" (map pretty_classrel clsses),
   56.12        pretty_default default,
    57.1 --- a/src/Pure/proofterm.ML	Sun May 06 21:50:17 2007 +0200
    57.2 +++ b/src/Pure/proofterm.ML	Mon May 07 00:49:59 2007 +0200
    57.3 @@ -110,8 +110,6 @@
    57.4      (string * (typ list -> proof -> proof option)) list -> proof -> proof
    57.5    val rewrite_proof_notypes : (proof * proof) list *
    57.6      (string * (typ list -> proof -> proof option)) list -> proof -> proof
    57.7 -  val init_data: theory -> theory
    57.8 -
    57.9  end
   57.10  
   57.11  structure Proofterm : PROOFTERM =
   57.12 @@ -1178,10 +1176,8 @@
   57.13  (**** theory data ****)
   57.14  
   57.15  structure ProofData = TheoryDataFun
   57.16 -(struct
   57.17 -  val name = "Pure/proof";
   57.18 -  type T = ((proof * proof) list *
   57.19 -    (string * (typ list -> proof -> proof option)) list);
   57.20 +(
   57.21 +  type T = (proof * proof) list * (string * (typ list -> proof -> proof option)) list;
   57.22  
   57.23    val empty = ([], []);
   57.24    val copy = I;
   57.25 @@ -1189,10 +1185,7 @@
   57.26    fun merge _ ((rules1, procs1) : T, (rules2, procs2)) =
   57.27      (Library.merge (op =) (rules1, rules2),
   57.28        AList.merge (op =) (K true) (procs1, procs2));
   57.29 -  fun print _ _ = ();
   57.30 -end);
   57.31 -
   57.32 -val init_data = ProofData.init;
   57.33 +);
   57.34  
   57.35  fun add_prf_rrule r = (ProofData.map o apfst) (insert (op =) r);
   57.36  
    58.1 --- a/src/Pure/pure_thy.ML	Sun May 06 21:50:17 2007 +0200
    58.2 +++ b/src/Pure/pure_thy.ML	Mon May 07 00:49:59 2007 +0200
    58.3 @@ -152,7 +152,6 @@
    58.4  
    58.5  structure TheoremsData = TheoryDataFun
    58.6  (struct
    58.7 -  val name = "Pure/theorems";
    58.8    type T =
    58.9     {theorems: thm list NameSpace.table,
   58.10      index: FactIndex.T} ref;
   58.11 @@ -505,9 +504,6 @@
   58.12  val proto_pure =
   58.13    Context.pre_pure_thy
   58.14    |> Compress.init_data
   58.15 -  |> Sign.init_data
   58.16 -  |> Theory.init_data
   58.17 -  |> Proofterm.init_data
   58.18    |> TheoremsData.init
   58.19    |> Sign.add_types
   58.20     [("fun", 2, NoSyn),
    59.1 --- a/src/Pure/sign.ML	Sun May 06 21:50:17 2007 +0200
    59.2 +++ b/src/Pure/sign.ML	Mon May 07 00:49:59 2007 +0200
    59.3 @@ -60,7 +60,6 @@
    59.4  
    59.5  signature SIGN =
    59.6  sig
    59.7 -  val init_data: theory -> theory
    59.8    val rep_sg: theory ->
    59.9     {naming: NameSpace.naming,
   59.10      syn: Syntax.syntax,
   59.11 @@ -203,8 +202,7 @@
   59.12    Sign {naming = naming, syn = syn, tsig = tsig, consts = consts};
   59.13  
   59.14  structure SignData = TheoryDataFun
   59.15 -(struct
   59.16 -  val name = "Pure/sign";
   59.17 +(
   59.18    type T = sign;
   59.19    val copy = I;
   59.20    fun extend (Sign {syn, tsig, consts, ...}) =
   59.21 @@ -223,11 +221,7 @@
   59.22        val tsig = Type.merge_tsigs pp (tsig1, tsig2);
   59.23        val consts = Consts.merge (consts1, consts2);
   59.24      in make_sign (naming, syn, tsig, consts) end;
   59.25 -
   59.26 -  fun print _ _ = ();
   59.27 -end);
   59.28 -
   59.29 -val init_data = SignData.init;
   59.30 +);
   59.31  
   59.32  fun rep_sg thy = SignData.get thy |> (fn Sign args => args);
   59.33  
    60.1 --- a/src/Pure/simplifier.ML	Sun May 06 21:50:17 2007 +0200
    60.2 +++ b/src/Pure/simplifier.ML	Mon May 07 00:49:59 2007 +0200
    60.3 @@ -97,19 +97,16 @@
    60.4  (* global simpsets *)
    60.5  
    60.6  structure GlobalSimpset = TheoryDataFun
    60.7 -(struct
    60.8 -  val name = "Pure/simpset";
    60.9 +(
   60.10    type T = simpset ref;
   60.11 -
   60.12    val empty = ref empty_ss;
   60.13 -  fun copy (ref ss) = ref ss: T;            (*create new reference!*)
   60.14 +  fun copy (ref ss) = ref ss: T;
   60.15    fun extend (ref ss) = ref (MetaSimplifier.inherit_context empty_ss ss);
   60.16    fun merge _ (ref ss1, ref ss2) = ref (merge_ss (ss1, ss2));
   60.17 -  fun print _ (ref ss) = print_ss ss;
   60.18 -end);
   60.19 +);
   60.20  
   60.21  val _ = Context.add_setup GlobalSimpset.init;
   60.22 -val print_simpset = GlobalSimpset.print;
   60.23 +fun print_simpset thy = print_ss (! (GlobalSimpset.get thy));
   60.24  val get_simpset = ! o GlobalSimpset.get;
   60.25  
   60.26  val change_simpset_of = change o GlobalSimpset.get;
   60.27 @@ -133,15 +130,12 @@
   60.28  (* local simpsets *)
   60.29  
   60.30  structure LocalSimpset = ProofDataFun
   60.31 -(struct
   60.32 -  val name = "Pure/simpset";
   60.33 +(
   60.34    type T = simpset;
   60.35    val init = get_simpset;
   60.36 -  fun print _ ss = print_ss ss;
   60.37 -end);
   60.38 +);
   60.39  
   60.40 -val _ = Context.add_setup LocalSimpset.init;
   60.41 -val print_local_simpset = LocalSimpset.print;
   60.42 +val print_local_simpset = print_ss o LocalSimpset.get;
   60.43  val get_local_simpset = LocalSimpset.get;
   60.44  val put_local_simpset = LocalSimpset.put;
   60.45  
   60.46 @@ -181,15 +175,12 @@
   60.47  
   60.48  structure Simprocs = GenericDataFun
   60.49  (
   60.50 -  val name = "Pure/simprocs";
   60.51    type T = simproc NameSpace.table;
   60.52    val empty = NameSpace.empty_table;
   60.53    val extend = I;
   60.54    fun merge _ simprocs = NameSpace.merge_tables eq_simproc simprocs
   60.55      handle Symtab.DUPS ds => err_dup_simprocs ds;
   60.56 -  fun print _ _ = ();
   60.57  );
   60.58 -val _ = Context.add_setup Simprocs.init;
   60.59  
   60.60  
   60.61  (* get simprocs *)
    61.1 --- a/src/Pure/theory.ML	Sun May 06 21:50:17 2007 +0200
    61.2 +++ b/src/Pure/theory.ML	Mon May 07 00:49:59 2007 +0200
    61.3 @@ -21,7 +21,6 @@
    61.4    val end_theory: theory -> theory
    61.5    val checkpoint: theory -> theory
    61.6    val copy: theory -> theory
    61.7 -  val init_data: theory -> theory
    61.8    val rep_theory: theory ->
    61.9     {axioms: term NameSpace.table,
   61.10      defs: Defs.T,
   61.11 @@ -101,8 +100,7 @@
   61.12  fun err_dup_oras dups = error ("Duplicate oracle(s): " ^ commas_quote dups);
   61.13  
   61.14  structure ThyData = TheoryDataFun
   61.15 -(struct
   61.16 -  val name = "Pure/theory";
   61.17 +(
   61.18    type T = thy;
   61.19    val empty = make_thy (NameSpace.empty_table, Defs.empty, NameSpace.empty_table);
   61.20    val copy = I;
   61.21 @@ -119,11 +117,7 @@
   61.22        val oracles = NameSpace.merge_tables (eq_snd (op =)) (oracles1, oracles2)
   61.23          handle Symtab.DUPS dups => err_dup_oras dups;
   61.24      in make_thy (axioms, defs, oracles) end;
   61.25 -
   61.26 -  fun print _ _ = ();
   61.27 -end);
   61.28 -
   61.29 -val init_data = ThyData.init;
   61.30 +);
   61.31  
   61.32  fun rep_theory thy = ThyData.get thy |> (fn Thy args => args);
   61.33  
    62.1 --- a/src/Pure/variable.ML	Sun May 06 21:50:17 2007 +0200
    62.2 +++ b/src/Pure/variable.ML	Mon May 07 00:49:59 2007 +0200
    62.3 @@ -79,15 +79,11 @@
    62.4  
    62.5  structure Data = ProofDataFun
    62.6  (
    62.7 -  val name = "Pure/variable";
    62.8    type T = data;
    62.9    fun init thy =
   62.10      make_data (false, Name.context, [], Vartab.empty, Symtab.empty, (Vartab.empty, Vartab.empty));
   62.11 -  fun print _ _ = ();
   62.12  );
   62.13  
   62.14 -val _ = Context.add_setup Data.init;
   62.15 -
   62.16  fun map_data f =
   62.17    Data.map (fn Data {is_body, names, fixes, binds, type_occs, constraints} =>
   62.18      make_data (f (is_body, names, fixes, binds, type_occs, constraints)));
    63.1 --- a/src/ZF/Tools/ind_cases.ML	Sun May 06 21:50:17 2007 +0200
    63.2 +++ b/src/ZF/Tools/ind_cases.ML	Mon May 07 00:49:59 2007 +0200
    63.3 @@ -19,16 +19,13 @@
    63.4  (* theory data *)
    63.5  
    63.6  structure IndCasesData = TheoryDataFun
    63.7 -(struct
    63.8 -  val name = "ZF/ind_cases";
    63.9 +(
   63.10    type T = (simpset -> cterm -> thm) Symtab.table;
   63.11 -
   63.12    val empty = Symtab.empty;
   63.13    val copy = I;
   63.14    val extend = I;
   63.15    fun merge _ tabs : T = Symtab.merge (K true) tabs;
   63.16 -  fun print _ _ = ();
   63.17 -end);
   63.18 +);
   63.19  
   63.20  
   63.21  fun declare name f = IndCasesData.map (Symtab.update (name, f));
   63.22 @@ -72,9 +69,8 @@
   63.23  (* package setup *)
   63.24  
   63.25  val setup =
   63.26 - (IndCasesData.init #>
   63.27 -  Method.add_methods [("ind_cases", mk_cases_meth oo mk_cases_args,
   63.28 -    "dynamic case analysis on sets")]);
   63.29 +  Method.add_methods
   63.30 +    [("ind_cases", mk_cases_meth oo mk_cases_args, "dynamic case analysis on sets")];
   63.31  
   63.32  
   63.33  (* outer syntax *)
    64.1 --- a/src/ZF/Tools/induct_tacs.ML	Sun May 06 21:50:17 2007 +0200
    64.2 +++ b/src/ZF/Tools/induct_tacs.ML	Mon May 07 00:49:59 2007 +0200
    64.3 @@ -31,19 +31,14 @@
    64.4     exhaustion : thm};
    64.5  
    64.6  structure DatatypesData = TheoryDataFun
    64.7 -(struct
    64.8 -  val name = "ZF/datatypes";
    64.9 +(
   64.10    type T = datatype_info Symtab.table;
   64.11 -
   64.12    val empty = Symtab.empty;
   64.13    val copy = I;
   64.14    val extend = I;
   64.15    fun merge _ tabs : T = Symtab.merge (K true) tabs;
   64.16 +);
   64.17  
   64.18 -  fun print thy tab =
   64.19 -    Pretty.writeln (Pretty.strs ("datatypes:" ::
   64.20 -      map #1 (NameSpace.extern_table (Sign.type_space thy, tab))));
   64.21 -end);
   64.22  
   64.23  
   64.24  (** Constructor information: needed to map constructors to datatypes **)
   64.25 @@ -56,15 +51,13 @@
   64.26  
   64.27  
   64.28  structure ConstructorsData = TheoryDataFun
   64.29 -(struct
   64.30 -  val name = "ZF/constructors"
   64.31 +(
   64.32    type T = constructor_info Symtab.table
   64.33    val empty = Symtab.empty
   64.34    val copy = I;
   64.35    val extend = I
   64.36    fun merge _ tabs: T = Symtab.merge (K true) tabs;
   64.37 -  fun print _ _= ();
   64.38 -end);
   64.39 +);
   64.40  
   64.41  structure DatatypeTactics : DATATYPE_TACTICS =
   64.42  struct
   64.43 @@ -185,13 +178,11 @@
   64.44  (* theory setup *)
   64.45  
   64.46  val setup =
   64.47 - (DatatypesData.init #>
   64.48 -  ConstructorsData.init #>
   64.49    Method.add_methods
   64.50      [("induct_tac", Method.goal_args Args.name induct_tac,
   64.51        "induct_tac emulation (dynamic instantiation!)"),
   64.52       ("case_tac", Method.goal_args Args.name exhaust_tac,
   64.53 -      "datatype case_tac emulation (dynamic instantiation!)")]);
   64.54 +      "datatype case_tac emulation (dynamic instantiation!)")];
   64.55  
   64.56  
   64.57  (* outer syntax *)
    65.1 --- a/src/ZF/Tools/typechk.ML	Sun May 06 21:50:17 2007 +0200
    65.2 +++ b/src/ZF/Tools/typechk.ML	Mon May 07 00:49:59 2007 +0200
    65.3 @@ -44,7 +44,6 @@
    65.4  
    65.5  structure Data = GenericDataFun
    65.6  (
    65.7 -  val name = "ZF/type-checking";
    65.8    type T = tcset
    65.9    val empty = TC {rules = [], net = Net.empty};
   65.10    val extend = I;
   65.11 @@ -52,19 +51,19 @@
   65.12    fun merge _ (TC {rules, net}, TC {rules = rules', net = net'}) =
   65.13      TC {rules = Drule.merge_rules (rules, rules'),
   65.14          net = Net.merge Thm.eq_thm_prop (net, net')};
   65.15 -
   65.16 -  fun print context (TC {rules, ...}) =
   65.17 -    Pretty.writeln (Pretty.big_list "type-checking rules:"
   65.18 -      (map (ProofContext.pretty_thm (Context.proof_of context)) rules));
   65.19  );
   65.20  
   65.21 -val print_tcset = Data.print o Context.Proof;
   65.22 -
   65.23  val TC_add = Thm.declaration_attribute (Data.map o add_rule);
   65.24  val TC_del = Thm.declaration_attribute (Data.map o del_rule);
   65.25  
   65.26  val tcset_of = Data.get o Context.Proof;
   65.27  
   65.28 +fun print_tcset ctxt =
   65.29 +  let val TC {rules, ...} = tcset_of ctxt in
   65.30 +    Pretty.writeln (Pretty.big_list "type-checking rules:"
   65.31 +      (map (ProofContext.pretty_thm ctxt) rules))
   65.32 +  end;
   65.33 +
   65.34  
   65.35  (* tactics *)
   65.36  
   65.37 @@ -128,7 +127,6 @@
   65.38  (* theory setup *)
   65.39  
   65.40  val setup =
   65.41 -  Data.init #>
   65.42    Attrib.add_attributes [("TC", TC_att, "declaration of type-checking rule")] #>
   65.43    Method.add_methods [("typecheck", typecheck_meth, "ZF type-checking")] #>
   65.44    (fn thy => (change_simpset_of thy (fn ss => ss setSolver type_solver); thy));