# HG changeset patch
# User wenzelm
# Date 1178491799 -7200
# Node ID fb79144af9a3da4980a2277b540a3e6ef6dbe619
# Parent  5f9138bcb3d75b731a5851e2c01134251ae80831
simplified DataFun interfaces;

diff -r 5f9138bcb3d7 -r fb79144af9a3 src/CCL/Wfd.thy
--- a/src/CCL/Wfd.thy	Sun May 06 21:50:17 2007 +0200
+++ b/src/CCL/Wfd.thy	Mon May 07 00:49:59 2007 +0200
@@ -500,12 +500,10 @@
 
 structure Data = GenericDataFun
 (
-  val name = "CCL/eval";
   type T = thm list;
   val empty = [];
   val extend = I;
   fun merge _ = Drule.merge_rules;
-  fun print _ _ = ();
 );
 
 in
@@ -518,7 +516,6 @@
     DEPTH_SOLVE_1 (resolve_tac (ths @ prems @ Data.get (Context.Proof ctxt)) 1)) 1;
 
 val eval_setup =
-  Data.init #>
   Attrib.add_attributes
     [("eval", Attrib.add_del_args eval_add eval_del, "declaration of evaluation rule")] #>
   Method.add_methods [("eval", Method.thms_ctxt_args (fn ths => fn ctxt =>
diff -r 5f9138bcb3d7 -r fb79144af9a3 src/HOL/Algebra/ringsimp.ML
--- a/src/HOL/Algebra/ringsimp.ML	Sun May 06 21:50:17 2007 +0200
+++ b/src/HOL/Algebra/ringsimp.ML	Mon May 07 00:49:59 2007 +0200
@@ -20,9 +20,8 @@
 fun struct_eq ((s1: string, ts1), (s2, ts2)) =
   (s1 = s2) andalso eq_list (op aconv) (ts1, ts2);
 
-structure AlgebraData = GenericDataFun
-(struct
-  val name = "Algebra/algebra";
+structure Data = GenericDataFun
+(
   type T = ((string * term list) * thm list) list;
     (* Algebraic structures:
        identifier of the structure, list of operations and simp rules,
@@ -30,20 +29,16 @@
   val empty = [];
   val extend = I;
   fun merge _ = AList.join struct_eq (K (Library.merge Thm.eq_thm_prop));
-  fun print generic structs =
-    let
-      val ctxt = Context.proof_of generic;
-      val pretty_term = Pretty.quote o ProofContext.pretty_term ctxt;
-      fun pretty_struct ((s, ts), _) = Pretty.block
-        [Pretty.str s, Pretty.str ":", Pretty.brk 1,
-         Pretty.enclose "(" ")" (Pretty.breaks (map pretty_term ts))];
-    in
-      Pretty.big_list "Algebraic structures:" (map pretty_struct structs) |>
-        Pretty.writeln
-    end
-end);
+);
 
-val print_structures = AlgebraData.print o Context.Proof;
+fun print_structures ctxt =
+  let
+    val structs = Data.get (Context.Proof ctxt);
+    val pretty_term = Pretty.quote o ProofContext.pretty_term ctxt;
+    fun pretty_struct ((s, ts), _) = Pretty.block
+      [Pretty.str s, Pretty.str ":", Pretty.brk 1,
+       Pretty.enclose "(" ")" (Pretty.breaks (map pretty_term ts))];
+  in Pretty.writeln (Pretty.big_list "Algebraic structures:" (map pretty_struct structs)) end;
 
 
 (** Method **)
@@ -57,17 +52,17 @@
   in asm_full_simp_tac (HOL_ss settermless less addsimps simps) end;
 
 fun algebra_tac ctxt =
-  EVERY' (map (fn s => TRY o struct_tac s) (AlgebraData.get (Context.Proof ctxt)));
+  EVERY' (map (fn s => TRY o struct_tac s) (Data.get (Context.Proof ctxt)));
 
 
 (** Attribute **)
 
 fun add_struct_thm s =
   Thm.declaration_attribute
-    (fn thm => AlgebraData.map (AList.map_default struct_eq (s, []) (insert Thm.eq_thm_prop thm)));
+    (fn thm => Data.map (AList.map_default struct_eq (s, []) (insert Thm.eq_thm_prop thm)));
 fun del_struct s =
   Thm.declaration_attribute
-    (fn _ => AlgebraData.map (AList.delete struct_eq s));
+    (fn _ => Data.map (AList.delete struct_eq s));
 
 val attribute = Attrib.syntax
      (Scan.lift ((Args.add >> K true || Args.del >> K false) --| Args.colon ||
@@ -79,7 +74,6 @@
 (** Setup **)
 
 val setup =
-  AlgebraData.init #>
   Method.add_methods [("algebra", Method.ctxt_args (Method.SIMPLE_METHOD' o algebra_tac),
     "normalisation of algebraic structure")] #>
   Attrib.add_attributes [("algebra", attribute, "theorems controlling algebra method")];
diff -r 5f9138bcb3d7 -r fb79144af9a3 src/HOL/Hyperreal/transfer.ML
--- a/src/HOL/Hyperreal/transfer.ML	Sun May 06 21:50:17 2007 +0200
+++ b/src/HOL/Hyperreal/transfer.ML	Mon May 07 00:49:59 2007 +0200
@@ -16,8 +16,7 @@
 struct
 
 structure TransferData = GenericDataFun
-(struct
-  val name = "HOL/transfer";
+(
   type T = {
     intros: thm list,
     unfolds: thm list,
@@ -35,8 +34,7 @@
     unfolds = Drule.merge_rules (unfolds1, unfolds2),
     refolds = Drule.merge_rules (refolds1, refolds2),
     consts = Library.merge (op =) (consts1, consts2)} : T;
-  fun print _ _ = ();
-end);
+);
 
 val transfer_start = thm "transfer_start"
 
@@ -109,7 +107,6 @@
     {intros=intros, unfolds=unfolds, refolds=refolds, consts=c::consts}))
 
 val setup =
-  TransferData.init #>
   Attrib.add_attributes
     [("transfer_intro", Attrib.add_del_args intro_add intro_del,
       "declaration of transfer introduction rule"),
diff -r 5f9138bcb3d7 -r fb79144af9a3 src/HOL/Import/hol4rews.ML
--- a/src/HOL/Import/hol4rews.ML	Sun May 06 21:50:17 2007 +0200
+++ b/src/HOL/Import/hol4rews.ML	Mon May 07 00:49:59 2007 +0200
@@ -12,102 +12,70 @@
        | Generating of string
        | Replaying of string
 
-structure HOL4DefThyArgs: THEORY_DATA_ARGS =
-struct
-val name = "HOL4/import_status"
-type T = ImportStatus
-val empty = NoImport
-val copy = I
-val extend = I
-fun merge _ (NoImport,NoImport) = NoImport
-  | merge _ _ = (warning "Import status set during merge"; NoImport)
-fun print _ import_status =
-    Pretty.writeln (Pretty.str (case import_status of NoImport => "No current import" | Generating thyname => ("Generating " ^ thyname) | Replaying thyname => ("Replaying " ^ thyname)))
-end;
-
-structure HOL4DefThy = TheoryDataFun(HOL4DefThyArgs);
+structure HOL4DefThy = TheoryDataFun
+(
+  type T = ImportStatus
+  val empty = NoImport
+  val copy = I
+  val extend = I
+  fun merge _ (NoImport,NoImport) = NoImport
+    | merge _ _ = (warning "Import status set during merge"; NoImport)
+)
 
-structure ImportSegmentArgs: THEORY_DATA_ARGS =
-struct
-val name = "HOL4/import_segment"
-type T = string
-val empty = ""
-val copy = I
-val extend = I
-fun merge _ ("",arg) = arg
-  | merge _ (arg,"") = arg
-  | merge _ (s1,s2) =
-    if s1 = s2
-    then s1
-    else error "Trying to merge two different import segments"
-fun print _ import_segment =
-    Pretty.writeln (Pretty.str ("Import segment: " ^ import_segment))
-end;
-
-structure ImportSegment = TheoryDataFun(ImportSegmentArgs);
+structure ImportSegment = TheoryDataFun
+(
+  type T = string
+  val empty = ""
+  val copy = I
+  val extend = I
+  fun merge _ ("",arg) = arg
+    | merge _ (arg,"") = arg
+    | merge _ (s1,s2) =
+      if s1 = s2
+      then s1
+      else error "Trying to merge two different import segments"
+)
 
 val get_import_segment = ImportSegment.get
 val set_import_segment = ImportSegment.put
 
-structure HOL4UNamesArgs: THEORY_DATA_ARGS =
-struct
-val name = "HOL4/used_names"
-type T = string list
-val empty = []
-val copy = I
-val extend = I
-fun merge _ ([],[]) = []
-  | merge _ _ = error "Used names not empty during merge"
-fun print _ used_names =
-    Pretty.writeln (Pretty.str "Printing of HOL4/used_names Not implemented")
-end;
-
-structure HOL4UNames = TheoryDataFun(HOL4UNamesArgs);
-
-structure HOL4DumpArgs: THEORY_DATA_ARGS =
-struct
-val name = "HOL4/dump_data"
-type T = string * string * string list
-val empty = ("","",[])
-val copy = I
-val extend = I
-fun merge _ (("","",[]),("","",[])) = ("","",[])
-  | merge _ _ = error "Dump data not empty during merge"
-fun print _ dump_data =
-    Pretty.writeln (Pretty.str "Printing of HOL4/dump_data Not implemented")
-end;
-
-structure HOL4Dump = TheoryDataFun(HOL4DumpArgs);
+structure HOL4UNames = TheoryDataFun
+(
+  type T = string list
+  val empty = []
+  val copy = I
+  val extend = I
+  fun merge _ ([],[]) = []
+    | merge _ _ = error "Used names not empty during merge"
+)
 
-structure HOL4MovesArgs: THEORY_DATA_ARGS =
-struct
-val name = "HOL4/moves"
-type T = string Symtab.table
-val empty = Symtab.empty
-val copy = I
-val extend = I
-fun merge _ : T * T -> T = Symtab.merge (K true)
-fun print _ tab =
-  Pretty.writeln (Pretty.big_list "HOL4 moves:"
-    (Symtab.fold (fn (bef, aft) => fn xl => (Pretty.str (bef ^ " --> " ^ aft) :: xl)) tab []))
-end;
-
-structure HOL4Moves = TheoryDataFun(HOL4MovesArgs);
+structure HOL4Dump = TheoryDataFun
+(
+  type T = string * string * string list
+  val empty = ("","",[])
+  val copy = I
+  val extend = I
+  fun merge _ (("","",[]),("","",[])) = ("","",[])
+    | merge _ _ = error "Dump data not empty during merge"
+)
 
-structure HOL4ImportsArgs: THEORY_DATA_ARGS =
-struct
-val name = "HOL4/imports"
-type T = string Symtab.table
-val empty = Symtab.empty
-val copy = I
-val extend = I
-fun merge _ : T * T -> T = Symtab.merge (K true)
-fun print _ tab =
-  Pretty.writeln (Pretty.big_list "HOL4 imports:"
-    (Symtab.fold (fn (thyname, segname) => fn xl => (Pretty.str (thyname ^ " imported from segment " ^ segname) :: xl)) tab []))
-end;
+structure HOL4Moves = TheoryDataFun
+(
+  type T = string Symtab.table
+  val empty = Symtab.empty
+  val copy = I
+  val extend = I
+  fun merge _ : T * T -> T = Symtab.merge (K true)
+)
 
-structure HOL4Imports = TheoryDataFun(HOL4ImportsArgs);
+structure HOL4Imports = TheoryDataFun
+(
+  type T = string Symtab.table
+  val empty = Symtab.empty
+  val copy = I
+  val extend = I
+  fun merge _ : T * T -> T = Symtab.merge (K true)
+)
 
 fun get_segment2 thyname thy =
   Symtab.lookup (HOL4Imports.get thy) thyname
@@ -120,143 +88,86 @@
 	HOL4Imports.put imps' thy
     end
 
-structure HOL4CMovesArgs: THEORY_DATA_ARGS =
-struct
-val name = "HOL4/constant_moves"
-type T = string Symtab.table
-val empty = Symtab.empty
-val copy = I
-val extend = I
-fun merge _ : T * T -> T = Symtab.merge (K true)
-fun print _ tab =
-  Pretty.writeln (Pretty.big_list "HOL4 constant moves:"
-    (Symtab.fold (fn (bef, aft) => fn xl => (Pretty.str (bef ^ " --> " ^ aft) :: xl)) tab []))
-end;
-
-structure HOL4CMoves = TheoryDataFun(HOL4CMovesArgs);
+structure HOL4CMoves = TheoryDataFun
+(
+  type T = string Symtab.table
+  val empty = Symtab.empty
+  val copy = I
+  val extend = I
+  fun merge _ : T * T -> T = Symtab.merge (K true)
+)
 
-structure HOL4MapsArgs: THEORY_DATA_ARGS =
-struct
-val name = "HOL4/mappings"
-type T = (string option) StringPair.table
-val empty = StringPair.empty
-val copy = I
-val extend = I
-fun merge _ : T * T -> T = StringPair.merge (K true)
-fun print _ tab =
-  Pretty.writeln (Pretty.big_list "HOL4 mappings:"
-    (StringPair.fold (fn ((bthy, bthm), isathm) => fn xl =>
-      (Pretty.str (bthy ^ "." ^ bthm ^ (case isathm of SOME th => " --> " ^ th | NONE => "IGNORED")) :: xl)) tab []))
-end;
-
-structure HOL4Maps = TheoryDataFun(HOL4MapsArgs);
+structure HOL4Maps = TheoryDataFun
+(
+  type T = (string option) StringPair.table
+  val empty = StringPair.empty
+  val copy = I
+  val extend = I
+  fun merge _ : T * T -> T = StringPair.merge (K true)
+)
 
-structure HOL4ThmsArgs: THEORY_DATA_ARGS =
-struct
-val name = "HOL4/theorems"
-type T = holthm StringPair.table
-val empty = StringPair.empty
-val copy = I
-val extend = I
-fun merge _ : T * T -> T = StringPair.merge (K true)
-fun print _ tab =
-  Pretty.writeln (Pretty.big_list "HOL4 mappings:"
-    (StringPair.fold (fn ((bthy, bthm), (_, thm)) => fn xl => (Pretty.str (bthy ^ "." ^ bthm ^ ":") :: Display.pretty_thm thm :: xl)) tab []))
-end;
-
-structure HOL4Thms = TheoryDataFun(HOL4ThmsArgs);
+structure HOL4Thms = TheoryDataFun
+(
+  type T = holthm StringPair.table
+  val empty = StringPair.empty
+  val copy = I
+  val extend = I
+  fun merge _ : T * T -> T = StringPair.merge (K true)
+)
 
-structure HOL4ConstMapsArgs: THEORY_DATA_ARGS =
-struct
-val name = "HOL4/constmappings"
-type T = (bool * string * typ option) StringPair.table
-val empty = StringPair.empty
-val copy = I
-val extend = I
-fun merge _ : T * T -> T = StringPair.merge (K true)
-fun print _ tab =
-  Pretty.writeln (Pretty.big_list "HOL4 constant mappings:"
-    (StringPair.fold (fn ((bthy, bconst), (internal, isaconst, _)) => fn xl =>
-      (Pretty.str (bthy ^ "." ^ bconst ^ " --> " ^ isaconst ^ (if internal then " (*)" else "")) :: xl)) tab []))
-end;
-
-structure HOL4ConstMaps = TheoryDataFun(HOL4ConstMapsArgs);
+structure HOL4ConstMaps = TheoryDataFun
+(
+  type T = (bool * string * typ option) StringPair.table
+  val empty = StringPair.empty
+  val copy = I
+  val extend = I
+  fun merge _ : T * T -> T = StringPair.merge (K true)
+)
 
-structure HOL4RenameArgs: THEORY_DATA_ARGS =
-struct
-val name = "HOL4/renamings"
-type T = string StringPair.table
-val empty = StringPair.empty
-val copy = I
-val extend = I
-fun merge _ : T * T -> T = StringPair.merge (K true)
-fun print _ tab =
-  Pretty.writeln (Pretty.big_list "HOL4 constant renamings:"
-    (StringPair.fold (fn ((bthy,bconst),newname) => fn xl => (Pretty.str (bthy ^ "." ^ bconst ^ " --> " ^ newname)::xl)) tab []))
-end;
-
-structure HOL4Rename = TheoryDataFun(HOL4RenameArgs);
+structure HOL4Rename = TheoryDataFun
+(
+  type T = string StringPair.table
+  val empty = StringPair.empty
+  val copy = I
+  val extend = I
+  fun merge _ : T * T -> T = StringPair.merge (K true)
+)
 
-structure HOL4DefMapsArgs: THEORY_DATA_ARGS =
-struct
-val name = "HOL4/def_maps"
-type T = string StringPair.table
-val empty = StringPair.empty
-val copy = I
-val extend = I
-fun merge _ : T * T -> T = StringPair.merge (K true)
-fun print _ tab =
-  Pretty.writeln (Pretty.big_list "HOL4 constant definitions:"
-    (StringPair.fold (fn ((bthy,bconst),newname) => fn xl => (Pretty.str (bthy ^ "." ^ bconst ^ ": " ^ newname)::xl)) tab []))
-end;
-
-structure HOL4DefMaps = TheoryDataFun(HOL4DefMapsArgs);
+structure HOL4DefMaps = TheoryDataFun
+(
+  type T = string StringPair.table
+  val empty = StringPair.empty
+  val copy = I
+  val extend = I
+  fun merge _ : T * T -> T = StringPair.merge (K true)
+)
 
-structure HOL4TypeMapsArgs: THEORY_DATA_ARGS =
-struct
-val name = "HOL4/typemappings"
-type T = (bool * string) StringPair.table
-val empty = StringPair.empty
-val copy = I
-val extend = I
-fun merge _ : T * T -> T = StringPair.merge (K true)
-fun print _ tab =
-  Pretty.writeln (Pretty.big_list "HOL4 type mappings:"
-    (StringPair.fold (fn ((bthy, bconst), (internal, isaconst)) => fn xl =>
-      (Pretty.str (bthy ^ "." ^ bconst ^ " --> " ^ isaconst ^ (if internal then " (*)" else "")) :: xl)) tab []))
-end;
-
-structure HOL4TypeMaps = TheoryDataFun(HOL4TypeMapsArgs);
+structure HOL4TypeMaps = TheoryDataFun
+(
+  type T = (bool * string) StringPair.table
+  val empty = StringPair.empty
+  val copy = I
+  val extend = I
+  fun merge _ : T * T -> T = StringPair.merge (K true)
+)
 
-structure HOL4PendingArgs: THEORY_DATA_ARGS =
-struct
-val name = "HOL4/pending"
-type T = ((term * term) list * thm) StringPair.table
-val empty = StringPair.empty
-val copy = I
-val extend = I
-fun merge _ : T * T -> T = StringPair.merge (K true)
-fun print _ tab =
-    Pretty.writeln (Pretty.big_list "HOL4 pending theorems:"
-	(StringPair.fold (fn ((bthy,bthm),(_,th)) => fn xl => (Pretty.chunks [Pretty.str (bthy ^ "." ^ bthm ^ ":"),Display.pretty_thm th]::xl)) tab []))
-end;
-
-structure HOL4Pending = TheoryDataFun(HOL4PendingArgs);
+structure HOL4Pending = TheoryDataFun
+(
+  type T = ((term * term) list * thm) StringPair.table
+  val empty = StringPair.empty
+  val copy = I
+  val extend = I
+  fun merge _ : T * T -> T = StringPair.merge (K true)
+)
 
-structure HOL4RewritesArgs: THEORY_DATA_ARGS =
-struct
-val name = "HOL4/rewrites"
-type T = thm list
-val empty = []
-val copy = I
-val extend = I
-fun merge _ = Library.gen_union Thm.eq_thm
-fun print _ thms =
-    Pretty.writeln (Pretty.big_list "HOL4 rewrite rules:"
-				    (map Display.pretty_thm thms))
-end;
-
-structure HOL4Rewrites = TheoryDataFun(HOL4RewritesArgs);
+structure HOL4Rewrites = TheoryDataFun
+(
+  type T = thm list
+  val empty = []
+  val copy = I
+  val extend = I
+  fun merge _ = Library.gen_union Thm.eq_thm
+)
 
 val hol4_debug = ref false
 fun message s = if !hol4_debug then writeln s else ()
@@ -677,7 +588,7 @@
 	  | _ => error "hol4rews.set_used_names called on initialized data!"
     end
 
-val clear_used_names = HOL4UNames.put HOL4UNamesArgs.empty
+val clear_used_names = HOL4UNames.put [];
 
 fun get_defmap thyname const thy =
     let
@@ -737,21 +648,6 @@
 	    |> add_hol4_const_mapping "min" "@" false "Hilbert_Choice.Eps"
 in
 val hol4_setup =
-  HOL4Rewrites.init #>
-  HOL4Maps.init #>
-  HOL4UNames.init #>
-  HOL4DefMaps.init #>
-  HOL4Moves.init #>
-  HOL4CMoves.init #>
-  HOL4ConstMaps.init #>
-  HOL4Rename.init #>
-  HOL4TypeMaps.init #>
-  HOL4Pending.init #>
-  HOL4Thms.init #>
-  HOL4Dump.init #>
-  HOL4DefThy.init #>
-  HOL4Imports.init #>
-  ImportSegment.init #>
   initial_maps #>
   Attrib.add_attributes
     [("hol4rew", Attrib.no_args add_hol4_rewrite, "HOL4 rewrite rule")]
diff -r 5f9138bcb3d7 -r fb79144af9a3 src/HOL/Import/import_package.ML
--- a/src/HOL/Import/import_package.ML	Sun May 06 21:50:17 2007 +0200
+++ b/src/HOL/Import/import_package.ML	Mon May 07 00:49:59 2007 +0200
@@ -10,18 +10,14 @@
     val debug      : bool ref
 end
 
-structure ImportDataArgs: THEORY_DATA_ARGS =
-struct
-val name = "HOL4/import_data"
-type T = ProofKernel.thm option array option
-val empty = NONE
-val copy = I
-val extend = I
-fun merge _ _ = NONE
-fun print _ _ = ()
-end
-
-structure ImportData = TheoryDataFun(ImportDataArgs)
+structure ImportData = TheoryDataFun
+(
+  type T = ProofKernel.thm option array option
+  val empty = NONE
+  val copy = I
+  val extend = I
+  fun merge _ _ = NONE
+)
 
 structure ImportPackage :> IMPORT_PACKAGE =
 struct
@@ -80,6 +76,6 @@
                           Method.SIMPLE_METHOD (import_tac arg thy)
                       end)
 
-val setup = Method.add_method("import",import_meth,"Import HOL4 theorem") #> ImportData.init
+val setup = Method.add_method("import",import_meth,"Import HOL4 theorem")
 end
 
diff -r 5f9138bcb3d7 -r fb79144af9a3 src/HOL/Import/shuffler.ML
--- a/src/HOL/Import/shuffler.ML	Sun May 06 21:50:17 2007 +0200
+++ b/src/HOL/Import/shuffler.ML	Mon May 07 00:49:59 2007 +0200
@@ -75,20 +75,18 @@
        | _ => raise THM("Not an equality",0,[th]))
     handle _ => raise THM("Couldn't make object equality",0,[th])
 
-structure ShuffleDataArgs: THEORY_DATA_ARGS =
-struct
-val name = "HOL/shuffles"
-type T = thm list
-val empty = []
-val copy = I
-val extend = I
-fun merge _ = Library.gen_union Thm.eq_thm
-fun print _ thms =
-    Pretty.writeln (Pretty.big_list "Shuffle theorems:"
-                                    (map Display.pretty_thm thms))
-end
+structure ShuffleData = TheoryDataFun
+(
+  type T = thm list
+  val empty = []
+  val copy = I
+  val extend = I
+  fun merge _ = Library.gen_union Thm.eq_thm
+)
 
-structure ShuffleData = TheoryDataFun(ShuffleDataArgs)
+fun print_shuffles thy =
+  Pretty.writeln (Pretty.big_list "Shuffle theorems:"
+    (map Display.pretty_thm (ShuffleData.get thy)))
 
 val weaken =
     let
@@ -667,8 +665,6 @@
         Method.SIMPLE_METHOD' (gen_shuffle_tac thy true (map (pair "premise") prems))
     end
 
-val print_shuffles = ShuffleData.print
-
 fun add_shuffle_rule thm thy =
     let
         val shuffles = ShuffleData.get thy
@@ -682,9 +678,10 @@
 val shuffle_attr = Thm.declaration_attribute (fn th => Context.mapping (add_shuffle_rule th) I);
 
 val setup =
-  Method.add_method ("shuffle_tac",Method.thms_ctxt_args shuffle_meth,"solve goal by shuffling terms around") #>
-  Method.add_method ("search_tac",Method.ctxt_args search_meth,"search for suitable theorems") #>
-  ShuffleData.init #>
+  Method.add_method ("shuffle_tac",
+    Method.thms_ctxt_args shuffle_meth,"solve goal by shuffling terms around") #>
+  Method.add_method ("search_tac",
+    Method.ctxt_args search_meth,"search for suitable theorems") #>
   add_shuffle_rule weaken #>
   add_shuffle_rule equiv_comm #>
   add_shuffle_rule imp_comm #>
diff -r 5f9138bcb3d7 -r fb79144af9a3 src/HOL/Inductive.thy
--- a/src/HOL/Inductive.thy	Sun May 06 21:50:17 2007 +0200
+++ b/src/HOL/Inductive.thy	Mon May 07 00:49:59 2007 +0200
@@ -118,7 +118,6 @@
 use "Tools/datatype_realizer.ML"
 
 use "Tools/datatype_hooks.ML"
-setup DatatypeHooks.setup
 
 use "Tools/datatype_package.ML"
 setup DatatypePackage.setup
diff -r 5f9138bcb3d7 -r fb79144af9a3 src/HOL/Nominal/Nominal.thy
--- a/src/HOL/Nominal/Nominal.thy	Sun May 06 21:50:17 2007 +0200
+++ b/src/HOL/Nominal/Nominal.thy	Mon May 07 00:49:59 2007 +0200
@@ -3226,7 +3226,6 @@
 (* setup for the individial atom-kinds *)
 (* and nominal datatypes               *)
 use "nominal_atoms.ML"
-setup "NominalAtoms.setup"
 
 (************************************************************)
 (* various tactics for analysing permutations, supports etc *)
@@ -3288,7 +3287,6 @@
 (************************************************)
 (* main file for constructing nominal datatypes *)
 use "nominal_package.ML"
-setup "NominalPackage.setup"
 
 (******************************************************)
 (* primitive recursive functions on nominal datatypes *)
diff -r 5f9138bcb3d7 -r fb79144af9a3 src/HOL/Nominal/nominal_atoms.ML
--- a/src/HOL/Nominal/nominal_atoms.ML	Sun May 06 21:50:17 2007 +0200
+++ b/src/HOL/Nominal/nominal_atoms.ML	Mon May 07 00:49:59 2007 +0200
@@ -13,7 +13,6 @@
   val get_atom_info : theory -> string -> atom_info option
   val atoms_of : theory -> string list
   val mk_permT : typ -> typ
-  val setup : theory -> theory
 end
 
 structure NominalAtoms : NOMINAL_ATOMS =
@@ -23,27 +22,21 @@
 val Collect_const = thm "Collect_const";
 
 
-(* data kind 'HOL/nominal' *)
+(* theory data *)
 
 type atom_info =
   {pt_class : string,
    fs_class : string,
    cp_classes : (string * string) list};
 
-structure NominalArgs =
-struct
-  val name = "HOL/nominal";
+structure NominalData = TheoryDataFun
+(
   type T = atom_info Symtab.table;
-
   val empty = Symtab.empty;
   val copy = I;
   val extend = I;
   fun merge _ x = Symtab.merge (K true) x;
-
-  fun print sg tab = ();
-end;
-
-structure NominalData = TheoryDataFun(NominalArgs);
+);
 
 fun make_atom_info ((pt_class, fs_class), cp_classes) =
   {pt_class = pt_class,
@@ -889,6 +882,4 @@
 
 val _ = OuterSyntax.add_parsers [atom_declP];
 
-val setup = NominalData.init;
-
 end;
diff -r 5f9138bcb3d7 -r fb79144af9a3 src/HOL/Nominal/nominal_package.ML
--- a/src/HOL/Nominal/nominal_package.ML	Sun May 06 21:50:17 2007 +0200
+++ b/src/HOL/Nominal/nominal_package.ML	Mon May 07 00:49:59 2007 +0200
@@ -17,7 +17,6 @@
   val perm_of_pair: term * term -> term
   val mk_not_sym: thm list -> thm list
   val perm_simproc: simproc
-  val setup: theory -> theory
 end
 
 structure NominalPackage : NOMINAL_PACKAGE =
@@ -68,7 +67,7 @@
 
 end;
 
-(* data kind 'HOL/nominal_datatypes' *)
+(* theory data *)
 
 type descr = (int * (string * dtyp list * (string * (dtyp list * dtyp) list) list)) list;
 
@@ -83,25 +82,19 @@
    inject : thm list};
 
 structure NominalDatatypesData = TheoryDataFun
-(struct
-  val name = "HOL/nominal_datatypes";
+(
   type T = nominal_datatype_info Symtab.table;
-
   val empty = Symtab.empty;
   val copy = I;
   val extend = I;
   fun merge _ tabs : T = Symtab.merge (K true) tabs;
-
-  fun print sg tab =
-    Pretty.writeln (Pretty.strs ("nominal datatypes:" ::
-      map #1 (NameSpace.extern_table (Sign.type_space sg, tab))));
-end);
+);
 
 val get_nominal_datatypes = NominalDatatypesData.get;
 val put_nominal_datatypes = NominalDatatypesData.put;
 val map_nominal_datatypes = NominalDatatypesData.map;
 val get_nominal_datatype = Symtab.lookup o get_nominal_datatypes;
-val setup = NominalDatatypesData.init;
+
 
 (**** make datatype info ****)
 
diff -r 5f9138bcb3d7 -r fb79144af9a3 src/HOL/Nominal/nominal_thmdecls.ML
--- a/src/HOL/Nominal/nominal_thmdecls.ML	Sun May 06 21:50:17 2007 +0200
+++ b/src/HOL/Nominal/nominal_thmdecls.ML	Mon May 07 00:49:59 2007 +0200
@@ -1,13 +1,13 @@
 (* ID: "$Id$"
    Authors: Julien Narboux and Christian Urban
 
-   This file introduces the infrastructure for the lemma 
+   This file introduces the infrastructure for the lemma
    declaration "eqvts" "bijs" and "freshs".
 
-   By attaching [eqvt] [bij] or [fresh] to a lemma, the lemma gets stored 
+   By attaching [eqvt] [bij] or [fresh] to a lemma, the lemma gets stored
    in a data-slot in the theory context. Possible modifiers
    are [attribute add] and [attribute del] for adding and deleting,
-   respectively the lemma from the data-slot.  
+   respectively the lemma from the data-slot.
 *)
 
 signature NOMINAL_THMDECLS =
@@ -21,7 +21,7 @@
   val get_eqvt_thms: theory -> thm list
   val get_fresh_thms: theory -> thm list
   val get_bij_thms: theory -> thm list
-  
+
 
   val NOMINAL_EQVT_DEBUG : bool ref
 end;
@@ -31,24 +31,12 @@
 
 structure Data = GenericDataFun
 (
-  val name = "HOL/Nominal/eqvt";
   type T = {eqvts:thm list, freshs:thm list, bijs:thm list};
   val empty = ({eqvts=[], freshs=[], bijs=[]}:T);
   val extend = I;
-  fun merge _ (r1:T,r2:T) = {eqvts  = Drule.merge_rules (#eqvts r1, #eqvts r2), 
-                             freshs = Drule.merge_rules (#freshs r1, #freshs r2), 
+  fun merge _ (r1:T,r2:T) = {eqvts  = Drule.merge_rules (#eqvts r1, #eqvts r2),
+                             freshs = Drule.merge_rules (#freshs r1, #freshs r2),
                              bijs   = Drule.merge_rules (#bijs r1, #bijs r2)}
-  fun print context (data:T) =
-    let 
-       fun print_aux msg thms =
-         Pretty.writeln (Pretty.big_list msg
-           (map (ProofContext.pretty_thm (Context.proof_of context)) thms))
-    in
-      (print_aux "Equivariance lemmas: " (#eqvts data);
-       print_aux "Freshness lemmas: " (#freshs data);
-       print_aux "Bijection lemmas: " (#bijs data))
-    end;
- 
 );
 
 (* Exception for when a theorem does not conform with form of an equivariance lemma. *)
@@ -62,7 +50,19 @@
 (* eqality-lemma can be derived. *)
 exception EQVT_FORM of string;
 
-val print_data = Data.print o Context.Proof;
+fun print_data ctxt =
+  let
+    val data = Data.get (Context.Proof ctxt);
+    fun pretty_thms msg thms =
+      Pretty.big_list msg (map (ProofContext.pretty_thm ctxt) thms);
+  in
+    Pretty.writeln (Pretty.chunks
+     [pretty_thms "Equivariance lemmas:" (#eqvts data),
+      pretty_thms "Freshness lemmas:" (#freshs data),
+      pretty_thms "Bijection lemmas:" (#bijs data)])
+  end;
+
+
 val get_eqvt_thms = Context.Theory #> Data.get #> #eqvts;
 val get_fresh_thms = Context.Theory #> Data.get #> #freshs;
 val get_bij_thms = Context.Theory #> Data.get #> #bijs;
@@ -75,56 +75,56 @@
 
 val NOMINAL_EQVT_DEBUG = ref false;
 
-fun tactic (msg,tac) = 
-    if !NOMINAL_EQVT_DEBUG 
+fun tactic (msg,tac) =
+    if !NOMINAL_EQVT_DEBUG
     then (EVERY [tac, print_tac ("after "^msg)])
-    else tac 
+    else tac
 
 fun dynamic_thms thy name = PureThy.get_thms thy (Name name)
 
-fun tactic_eqvt ctx orig_thm pi typi = 
-    let 
+fun tactic_eqvt ctx orig_thm pi typi =
+    let
         val mypi = Thm.cterm_of ctx (Var (pi,typi))
         val mypifree = Thm.cterm_of ctx (Const ("List.rev",typi --> typi) $ Free (fst pi,typi))
         val perm_pi_simp = dynamic_thms ctx "perm_pi_simp"
     in
-        EVERY [tactic ("iffI applied",rtac iffI 1), 
-               tactic ("simplifies with orig_thm and perm_bool", 
-                          asm_full_simp_tac (HOL_basic_ss addsimps [perm_bool,orig_thm]) 1), 
+        EVERY [tactic ("iffI applied",rtac iffI 1),
+               tactic ("simplifies with orig_thm and perm_bool",
+                          asm_full_simp_tac (HOL_basic_ss addsimps [perm_bool,orig_thm]) 1),
                tactic ("applies orig_thm instantiated with rev pi",
-                          dtac (Drule.cterm_instantiate [(mypi,mypifree)] orig_thm) 1), 
+                          dtac (Drule.cterm_instantiate [(mypi,mypifree)] orig_thm) 1),
                tactic ("getting rid of all remaining perms",
-                          full_simp_tac (HOL_basic_ss addsimps (perm_bool::perm_pi_simp)) 1)] 
+                          full_simp_tac (HOL_basic_ss addsimps (perm_bool::perm_pi_simp)) 1)]
     end;
 
 fun get_derived_thm thy hyp concl orig_thm pi typi =
-   let 
+   let
        val lhs = (Const("Nominal.perm", typi --> HOLogic.boolT --> HOLogic.boolT) $ Var(pi,typi) $ hyp)
-       val goal_term = Logic.unvarify (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs,concl))) 
-       val _ = Display.print_cterm (cterm_of thy goal_term) 
+       val goal_term = Logic.unvarify (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs,concl)))
+       val _ = Display.print_cterm (cterm_of thy goal_term)
    in	
-     Goal.prove_global thy [] [] goal_term (fn _ => (tactic_eqvt thy orig_thm pi typi)) 
+     Goal.prove_global thy [] [] goal_term (fn _ => (tactic_eqvt thy orig_thm pi typi))
    end
 
 (* FIXME: something naughty here, but as long as there is no infrastructure to expose *)
 (* the eqvt_thm_list to the user, we have to manually update the context and the      *)
 (* thm-list eqvt *)
 fun update_context flag thms context =
-  let 
-     val context' = fold (fn thm => Data.map (flag thm)) thms context 
-  in 
+  let
+     val context' = fold (fn thm => Data.map (flag thm)) thms context
+  in
     Context.mapping (snd o PureThy.add_thmss [(("eqvts",(#eqvts (Data.get context'))),[])]) I context'
   end;
 
-(* replaces every variable x in t with pi o x *) 
+(* replaces every variable x in t with pi o x *)
 fun apply_pi trm (pi,typi) =
-  let 
+  let
     fun only_vars t =
        (case t of
           Var (n,ty) => (Const ("Nominal.perm",typi --> ty --> ty) $ (Var (pi,typi)) $ (Var (n,ty)))
         | _ => t)
-  in 
-     map_aterms only_vars trm 
+  in
+     map_aterms only_vars trm
   end;
 
 (* returns *the* pi which is in front of all variables, provided there *)
@@ -132,69 +132,69 @@
 fun get_pi t thy =
   let fun get_pi_aux s =
         (case s of
-          (Const ("Nominal.perm",typrm) $ 
-             (Var (pi,typi as Type("List.list",[Type ("*",[Type (tyatm,[]),_])]))) $ 
-               (Var (n,ty))) => 
+          (Const ("Nominal.perm",typrm) $
+             (Var (pi,typi as Type("List.list",[Type ("*",[Type (tyatm,[]),_])]))) $
+               (Var (n,ty))) =>
              let
 		(* FIXME: this should be an operation the library *)
-                val class_name = (NameSpace.map_base (fn s => "pt_"^s) tyatm) 
-	     in 
-		if (Type.of_sort (Sign.tsig_of thy) (ty,[class_name])) 
-                then [(pi,typi)] 
-                else raise 
-                EQVT_FORM ("Could not find any permutation or an argument is not an instance of "^class_name) 
-             end 
+                val class_name = (NameSpace.map_base (fn s => "pt_"^s) tyatm)
+	     in
+		if (Type.of_sort (Sign.tsig_of thy) (ty,[class_name]))
+                then [(pi,typi)]
+                else raise
+                EQVT_FORM ("Could not find any permutation or an argument is not an instance of "^class_name)
+             end
         | Abs (_,_,t1) => get_pi_aux t1
         | (t1 $ t2) => get_pi_aux t1 @ get_pi_aux t2
-        | _ => [])  
-  in 
+        | _ => [])
+  in
     (* collect first all pi's in front of variables in t and then use distinct *)
     (* to ensure that all pi's must have been the same, i.e. distinct returns  *)
     (* a singleton-list  *)
-    (case (distinct (op =) (get_pi_aux t)) of 
+    (case (distinct (op =) (get_pi_aux t)) of
       [(pi,typi)] => (pi,typi)
     | _ => raise EQVT_FORM "All permutation should be the same")
   end;
 
 (* Either adds a theorem (orig_thm) to or deletes one from the equivaraince *)
 (* lemma list depending on flag. To be added the lemma has to satisfy a     *)
-(* certain form. *) 
+(* certain form. *)
 fun eqvt_add_del_aux flag orig_thm context =
-  let 
+  let
     val thy = Context.theory_of context
     val thms_to_be_added = (case (prop_of orig_thm) of
-        (* case: eqvt-lemma is of the implicational form *) 
+        (* case: eqvt-lemma is of the implicational form *)
         (Const("==>", _) $ (Const ("Trueprop",_) $ hyp) $ (Const ("Trueprop",_) $ concl)) =>
-          let  
+          let
             val (pi,typi) = get_pi concl thy
           in
              if (apply_pi hyp (pi,typi) = concl)
-             then 
+             then
                (warning ("equivariance lemma of the relational form");
                 [orig_thm, get_derived_thm thy hyp concl orig_thm pi typi])
              else raise EQVT_FORM "Type Implication"
           end
-       (* case: eqvt-lemma is of the equational form *)  
-      | (Const ("Trueprop", _) $ (Const ("op =", _) $ 
+       (* case: eqvt-lemma is of the equational form *)
+      | (Const ("Trueprop", _) $ (Const ("op =", _) $
             (Const ("Nominal.perm",typrm) $ Var (pi,typi) $ lhs) $ rhs)) =>
-	   (if (apply_pi lhs (pi,typi)) = rhs 
+	   (if (apply_pi lhs (pi,typi)) = rhs
                then [orig_thm]
                else raise EQVT_FORM "Type Equality")
       | _ => raise EQVT_FORM "Type unknown")
-  in 
+  in
       update_context flag thms_to_be_added context
   end
-  handle EQVT_FORM s => 
+  handle EQVT_FORM s =>
       error (string_of_thm orig_thm ^ " does not comply with the form of an equivariance lemma ("^s^").")
 
 (* in cases of bij- and freshness, we just add the lemmas to the *)
-(* data-slot *) 
+(* data-slot *)
 
-fun simple_add_del_aux record_access name flag th context = 
-   let 
+fun simple_add_del_aux record_access name flag th context =
+   let
      val context' = Data.map (flag th) context
    in
-     Context.mapping (snd o PureThy.add_thmss [((name,(record_access (Data.get context'))),[])]) I context' 
+     Context.mapping (snd o PureThy.add_thmss [((name,(record_access (Data.get context'))),[])]) I context'
    end
 
 fun bij_add_del_aux f   = simple_add_del_aux #bijs "bijs" f
@@ -205,21 +205,20 @@
 fun fresh_map f th (r:Data.T) = {eqvts = #eqvts r, freshs = (f th (#freshs r)), bijs = #bijs r};
 fun bij_map f th (r:Data.T)   = {eqvts = #eqvts r, freshs = #freshs r, bijs = (f th (#bijs r))};
 
-val eqvt_add  = Thm.declaration_attribute (eqvt_add_del_aux (eqvt_map Drule.add_rule)); 
-val eqvt_del  = Thm.declaration_attribute (eqvt_add_del_aux (eqvt_map Drule.del_rule)); 
-val eqvt_force_add  = Thm.declaration_attribute (eqvt_force_add_del_aux (eqvt_map Drule.add_rule)); 
-val eqvt_force_del  = Thm.declaration_attribute (eqvt_force_add_del_aux (eqvt_map Drule.del_rule)); 
+val eqvt_add  = Thm.declaration_attribute (eqvt_add_del_aux (eqvt_map Drule.add_rule));
+val eqvt_del  = Thm.declaration_attribute (eqvt_add_del_aux (eqvt_map Drule.del_rule));
+val eqvt_force_add  = Thm.declaration_attribute (eqvt_force_add_del_aux (eqvt_map Drule.add_rule));
+val eqvt_force_del  = Thm.declaration_attribute (eqvt_force_add_del_aux (eqvt_map Drule.del_rule));
 
-val bij_add   = Thm.declaration_attribute (bij_add_del_aux (bij_map Drule.add_rule)); 
+val bij_add   = Thm.declaration_attribute (bij_add_del_aux (bij_map Drule.add_rule));
 val bij_del   = Thm.declaration_attribute (bij_add_del_aux (bij_map Drule.del_rule));
-val fresh_add = Thm.declaration_attribute (fresh_add_del_aux (fresh_map Drule.add_rule)); 
+val fresh_add = Thm.declaration_attribute (fresh_add_del_aux (fresh_map Drule.add_rule));
 val fresh_del = Thm.declaration_attribute (fresh_add_del_aux (fresh_map Drule.del_rule));
 
 
 
 val setup =
-  Data.init #>
-  Attrib.add_attributes 
+  Attrib.add_attributes
      [("eqvt",  Attrib.add_del_args eqvt_add eqvt_del,   "equivariance theorem declaration"),
       ("eqvt_force", Attrib.add_del_args eqvt_force_add eqvt_force_del,
                              "equivariance theorem declaration (without checking the form of the lemma)"),
@@ -227,11 +226,3 @@
       ("bij",   Attrib.add_del_args bij_add bij_del,     "bijection theorem declaration")];
 
 end;
-
-(* Thm.declaration_attribute has type (thm -> Context.generic -> Context.generic) -> attribute *)
-
-(* Drule.add_rule has type thm -> thm list -> thm list *)
-
-(* Data.map has type thm list -> thm list -> Context.generic -> Context.generic *)
-
-(* add_del_args is of type attribute -> attribute -> src -> attribute *)
\ No newline at end of file
diff -r 5f9138bcb3d7 -r fb79144af9a3 src/HOL/Predicate.thy
--- a/src/HOL/Predicate.thy	Sun May 06 21:50:17 2007 +0200
+++ b/src/HOL/Predicate.thy	Mon May 07 00:49:59 2007 +0200
@@ -152,14 +152,12 @@
 val rules2 = [split_set, mk_meta_eq mem_Collect_eq, mem_Collect2_eq];
 
 structure PredSetConvData = GenericDataFun
-(struct
-  val name = "HOL/pred_set_conv";
+(
   type T = thm list;
   val empty = [];
   val extend = I;
   fun merge _ = Drule.merge_rules;
-  fun print _ _ = ()
-end)
+);
 
 fun mk_attr ths1 ths2 f = Attrib.syntax (Attrib.thms >> (fn ths =>
   Thm.rule_attribute (fn ctxt => rew ths1 (map (f o Simpdata.mk_eq)
@@ -170,7 +168,7 @@
 
 in
 
-val _ = ML_Context.>> (PredSetConvData.init #>
+val _ = ML_Context.>> (
   Attrib.add_attributes
     [("pred_set_conv", pred_set_conv_att,
         "declare rules for converting between predicate and set notation"),
diff -r 5f9138bcb3d7 -r fb79144af9a3 src/HOL/Tools/datatype_hooks.ML
--- a/src/HOL/Tools/datatype_hooks.ML	Sun May 06 21:50:17 2007 +0200
+++ b/src/HOL/Tools/datatype_hooks.ML	Mon May 07 00:49:59 2007 +0200
@@ -7,49 +7,29 @@
 
 signature DATATYPE_HOOKS =
 sig
-  type hook = string list -> theory -> theory;
-  val add: hook -> theory -> theory;
-  val all: hook;
-  val setup: theory -> theory;
+  type hook = string list -> theory -> theory
+  val add: hook -> theory -> theory
+  val all: hook
 end;
 
 structure DatatypeHooks : DATATYPE_HOOKS =
 struct
 
-
-(* theory data *)
-
 type hook = string list -> theory -> theory;
-datatype T = T of (serial * hook) list;
-
-fun map_T f (T hooks) = T (f hooks);
-fun merge_T pp (T hooks1, T hooks2) =
-  T (AList.merge (op =) (K true) (hooks1, hooks2));
 
 structure DatatypeHooksData = TheoryDataFun
-(struct
-  val name = "HOL/datatype_hooks";
-  type T = T;
-  val empty = T [];
+(
+  type T = (serial * hook) list;
+  val empty = [];
   val copy = I;
   val extend = I;
-  val merge = merge_T;
-  fun print _ _ = ();
-end);
-
-
-(* interface *)
+  fun merge _ hooks : T = AList.merge (op =) (K true) hooks;
+);
 
 fun add hook =
-  DatatypeHooksData.map (map_T (cons (serial (), hook)));
+  DatatypeHooksData.map (cons (serial (), hook));
 
 fun all dtcos thy =
-  fold (fn (_, f) => f dtcos) ((fn T hooks => hooks) (DatatypeHooksData.get thy)) thy;
-
-
-(* theory setup *)
-
-val setup = DatatypeHooksData.init;
+  fold (fn (_, f) => f dtcos) (DatatypeHooksData.get thy) thy;
 
 end;
-
diff -r 5f9138bcb3d7 -r fb79144af9a3 src/HOL/Tools/datatype_package.ML
--- a/src/HOL/Tools/datatype_package.ML	Sun May 06 21:50:17 2007 +0200
+++ b/src/HOL/Tools/datatype_package.ML	Mon May 07 00:49:59 2007 +0200
@@ -85,11 +85,10 @@
 val quiet_mode = quiet_mode;
 
 
-(* data kind 'HOL/datatypes' *)
+(* theory data *)
 
 structure DatatypesData = TheoryDataFun
-(struct
-  val name = "HOL/datatypes";
+(
   type T =
     {types: datatype_info Symtab.table,
      constrs: datatype_info Symtab.table,
@@ -105,15 +104,14 @@
     {types = Symtab.merge (K true) (types1, types2),
      constrs = Symtab.merge (K true) (constrs1, constrs2),
      cases = Symtab.merge (K true) (cases1, cases2)};
-
-  fun print sg ({types, ...} : T) =
-    Pretty.writeln (Pretty.strs ("datatypes:" ::
-      map #1 (NameSpace.extern_table (Sign.type_space sg, types))));
-end);
+);
 
 val get_datatypes = #types o DatatypesData.get;
 val map_datatypes = DatatypesData.map;
-val print_datatypes = DatatypesData.print;
+
+fun print_datatypes thy =
+  Pretty.writeln (Pretty.strs ("datatypes:" ::
+    map #1 (NameSpace.extern_table (Sign.type_space thy, get_datatypes thy))));
 
 
 (** theory information about datatypes **)
@@ -933,7 +931,7 @@
 (* setup theory *)
 
 val setup =
-  DatatypesData.init #> Method.add_methods tactic_emulations #> simproc_setup #> trfun_setup;
+  Method.add_methods tactic_emulations #> simproc_setup #> trfun_setup;
 
 
 (* outer syntax *)
diff -r 5f9138bcb3d7 -r fb79144af9a3 src/HOL/Tools/function_package/fundef_common.ML
--- a/src/HOL/Tools/function_package/fundef_common.ML	Sun May 06 21:50:17 2007 +0200
+++ b/src/HOL/Tools/function_package/fundef_common.ML	Mon May 07 00:49:59 2007 +0200
@@ -78,30 +78,24 @@
     end
 
 structure FundefData = GenericDataFun
-(struct
-  val name = "HOL/function_def/data";
-  type T = (term * fundef_context_data) NetRules.T
-
+(
+  type T = (term * fundef_context_data) NetRules.T;
   val empty = NetRules.init
     (op aconv o pairself fst : (term * fundef_context_data) * (term * fundef_context_data) -> bool)
     fst;
   val copy = I;
   val extend = I;
   fun merge _ (tab1, tab2) = NetRules.merge (tab1, tab2)
-
-  fun print _ _ = ();
-end);
+);
 
 
 structure FundefCongs = GenericDataFun
-(struct
-    val name = "HOL/function_def/congs"
-    type T = thm list
-    val empty = []
-    val extend = I
-    fun merge _ = Drule.merge_rules
-    fun print  _ _ = ()
-end);
+(
+  type T = thm list
+  val empty = []
+  val extend = I
+  fun merge _ = Drule.merge_rules
+);
 
 
 (* Generally useful?? *)
@@ -143,14 +137,12 @@
 
 
 structure TerminationRule = GenericDataFun
-(struct
-    val name = "HOL/function_def/termination"
-    type T = thm list
-    val empty = []
-    val extend = I
-    fun merge _ = Drule.merge_rules
-    fun print  _ _ = ()
-end);
+(
+  type T = thm list
+  val empty = []
+  val extend = I
+  fun merge _ = Drule.merge_rules
+);
 
 val get_termination_rules = TerminationRule.get
 val store_termination_rule = TerminationRule.map o cons
diff -r 5f9138bcb3d7 -r fb79144af9a3 src/HOL/Tools/function_package/fundef_package.ML
--- a/src/HOL/Tools/function_package/fundef_package.ML	Sun May 06 21:50:17 2007 +0200
+++ b/src/HOL/Tools/function_package/fundef_package.ML	Mon May 07 00:49:59 2007 +0200
@@ -208,13 +208,11 @@
 (* setup *)
 
 val setup =
-    FundefData.init
-      #> FundefCongs.init
-      #> TerminationRule.init
-      #>  Attrib.add_attributes
-            [("fundef_cong", Attrib.add_del_args cong_add cong_del, "declaration of congruence rule for function definitions")]
-      #> setup_case_cong_hook
-      #> FundefRelation.setup
+  Attrib.add_attributes
+    [("fundef_cong", Attrib.add_del_args cong_add cong_del,
+      "declaration of congruence rule for function definitions")]
+  #> setup_case_cong_hook
+  #> FundefRelation.setup
 
 val get_congs = FundefCommon.get_fundef_congs o Context.Theory
 
diff -r 5f9138bcb3d7 -r fb79144af9a3 src/HOL/Tools/inductive_codegen.ML
--- a/src/HOL/Tools/inductive_codegen.ML	Sun May 06 21:50:17 2007 +0200
+++ b/src/HOL/Tools/inductive_codegen.ML	Mon May 07 00:49:59 2007 +0200
@@ -22,8 +22,7 @@
   Symtab.join (fn _ => AList.merge (Thm.eq_thm_prop) (K true)) tabs;
 
 structure CodegenData = TheoryDataFun
-(struct
-  val name = "HOL/inductive_codegen";
+(
   type T =
     {intros : (thm * (string * int)) list Symtab.table,
      graph : unit Graph.T,
@@ -37,8 +36,7 @@
     {intros = merge_rules (intros1, intros2),
      graph = Graph.merge (K true) (graph1, graph2),
      eqns = merge_rules (eqns1, eqns2)};
-  fun print _ _ = ();
-end);
+);
 
 
 fun warn thm = warning ("InductiveCodegen: Not a proper clause:\n" ^
@@ -653,7 +651,6 @@
 
 val setup =
   add_codegen "inductive" inductive_codegen #>
-  CodegenData.init #>
   add_attribute "ind" (Scan.option (Args.$$$ "target" |-- Args.colon |-- Args.name) --
     Scan.option (Args.$$$ "params" |-- Args.colon |-- Args.nat) >> uncurry add);
 
diff -r 5f9138bcb3d7 -r fb79144af9a3 src/HOL/Tools/inductive_package.ML
--- a/src/HOL/Tools/inductive_package.ML	Sun May 06 21:50:17 2007 +0200
+++ b/src/HOL/Tools/inductive_package.ML	Mon May 07 00:49:59 2007 +0200
@@ -86,7 +86,7 @@
 
 
 
-(** theory data **)
+(** context data **)
 
 type inductive_result =
   {preds: term list, defs: thm list, elims: thm list, raw_induct: thm,
@@ -106,28 +106,25 @@
   {names: string list, coind: bool} * inductive_result;
 
 structure InductiveData = GenericDataFun
-(struct
-  val name = "HOL/inductive";
+(
   type T = inductive_info Symtab.table * thm list;
-
   val empty = (Symtab.empty, []);
   val extend = I;
   fun merge _ ((tab1, monos1), (tab2, monos2)) =
     (Symtab.merge (K true) (tab1, tab2), Drule.merge_rules (monos1, monos2));
-
-  fun print context (tab, monos) =
-    let
-      val ctxt = Context.proof_of context;
-      val space = Consts.space_of (ProofContext.consts_of ctxt);
-    in
-      [Pretty.strs ("(co)inductives:" :: map #1 (NameSpace.extern_table (space, tab))),
-       Pretty.big_list "monotonicity rules:" (map (ProofContext.pretty_thm ctxt) monos)]
-      |> Pretty.chunks |> Pretty.writeln
-    end;
-end);
+);
 
 val get_inductives = InductiveData.get o Context.Proof;
-val print_inductives = InductiveData.print o Context.Proof;
+
+fun print_inductives ctxt =
+  let
+    val (tab, monos) = get_inductives ctxt;
+    val space = Consts.space_of (ProofContext.consts_of ctxt);
+  in
+    [Pretty.strs ("(co)inductives:" :: map #1 (NameSpace.extern_table (space, tab))),
+     Pretty.big_list "monotonicity rules:" (map (ProofContext.pretty_thm ctxt) monos)]
+    |> Pretty.chunks |> Pretty.writeln
+  end;
 
 
 (* get and put data *)
@@ -156,7 +153,7 @@
           (_ $ (_ $ (Const ("Not", _) $ _) $ _)) => []
         | _ => [thm' RS (thm' RS eq_to_mono2)]);
     fun dest_less_concl thm = dest_less_concl (thm RS le_funD)
-      handle THM _ => thm RS le_boolD      
+      handle THM _ => thm RS le_boolD
   in
     case concl of
       Const ("==", _) $ _ $ _ => eq2mono (thm RS meta_eq_to_obj_eq)
@@ -892,7 +889,6 @@
 (* setup theory *)
 
 val setup =
-  InductiveData.init #>
   Method.add_methods [("ind_cases2", ind_cases,   (* FIXME "ind_cases" (?) *)
     "dynamic case analysis on predicates")] #>
   Attrib.add_attributes [("mono2", Attrib.add_del_args mono_add mono_del,   (* FIXME "mono" *)
diff -r 5f9138bcb3d7 -r fb79144af9a3 src/HOL/Tools/old_inductive_package.ML
--- a/src/HOL/Tools/old_inductive_package.ML	Sun May 06 21:50:17 2007 +0200
+++ b/src/HOL/Tools/old_inductive_package.ML	Mon May 07 00:49:59 2007 +0200
@@ -37,7 +37,6 @@
     {defs: thm list, elims: thm list, raw_induct: thm, induct: thm,
      intrs: thm list, mk_cases: string -> thm, mono: thm, unfold: thm}) option
   val the_mk_cases: theory -> string -> string -> thm
-  val print_inductives: theory -> unit
   val mono_add: attribute
   val mono_del: attribute
   val get_monos: theory -> thm list
@@ -88,27 +87,14 @@
     induct: thm, intrs: thm list, mk_cases: string -> thm, mono: thm, unfold: thm};
 
 structure InductiveData = TheoryDataFun
-(struct
-  val name = "HOL/inductive";
+(
   type T = inductive_info Symtab.table * thm list;
-
   val empty = (Symtab.empty, []);
   val copy = I;
   val extend = I;
   fun merge _ ((tab1, monos1), (tab2, monos2)) =
     (Symtab.merge (K true) (tab1, tab2), Drule.merge_rules (monos1, monos2));
-
-  fun print thy (tab, monos) =
-    [Pretty.strs ("(co)inductives:" ::
-      map #1 (NameSpace.extern_table (Sign.const_space thy, tab))),
-     Pretty.big_list "monotonicity rules:" (map (Display.pretty_thm_sg thy) monos)]
-    |> Pretty.chunks |> Pretty.writeln;
-end);
-
-val print_inductives = InductiveData.print;
-
-
-(* get and put data *)
+);
 
 val get_inductive = Symtab.lookup o #1 o InductiveData.get;
 
@@ -871,7 +857,6 @@
 (* setup theory *)
 
 val setup =
-  InductiveData.init #>
   Method.add_methods [("ind_cases", mk_cases_meth oo mk_cases_args,
     "dynamic case analysis on sets")] #>
   Attrib.add_attributes [("mono", Attrib.add_del_args mono_add mono_del,
diff -r 5f9138bcb3d7 -r fb79144af9a3 src/HOL/Tools/recdef_package.ML
--- a/src/HOL/Tools/recdef_package.ML	Sun May 06 21:50:17 2007 +0200
+++ b/src/HOL/Tools/recdef_package.ML	Mon May 07 00:49:59 2007 +0200
@@ -8,7 +8,6 @@
 signature RECDEF_PACKAGE =
 sig
   val quiet_mode: bool ref
-  val print_recdefs: theory -> unit
   val get_recdef: theory -> string
     -> {simps: thm list, rules: thm list list, induct: thm, tcs: term list} option
   val get_hints: Proof.context -> {simps: thm list, congs: (string * thm) list, wfs: thm list}
@@ -97,10 +96,8 @@
 type recdef_info = {simps: thm list, rules: thm list list, induct: thm, tcs: term list};
 
 structure GlobalRecdefData = TheoryDataFun
-(struct
-  val name = "HOL/recdef";
+(
   type T = recdef_info Symtab.table * hints;
-
   val empty = (Symtab.empty, mk_hints ([], [], [])): T;
   val copy = I;
   val extend = I;
@@ -111,14 +108,7 @@
         mk_hints (Drule.merge_rules (simps1, simps2),
           AList.merge (op =) Thm.eq_thm (congs1, congs2),
           Drule.merge_rules (wfs1, wfs2)));
-
-  fun print thy (tab, hints) =
-    (Pretty.strs ("recdefs:" :: map #1 (NameSpace.extern_table (Sign.const_space thy, tab))) ::
-      pretty_hints hints) |> Pretty.chunks |> Pretty.writeln;
-end);
-
-val print_recdefs = GlobalRecdefData.print;
-
+);
 
 val get_recdef = Symtab.lookup o #1 o GlobalRecdefData.get;
 
@@ -135,12 +125,10 @@
 (* proof data *)
 
 structure LocalRecdefData = ProofDataFun
-(struct
-  val name = "HOL/recdef";
+(
   type T = hints;
   val init = get_global_hints;
-  fun print _ hints = pretty_hints hints |> Pretty.chunks |> Pretty.writeln;
-end);
+);
 
 val get_hints = LocalRecdefData.get;
 fun map_hints f = Context.mapping (GlobalRecdefData.map (apsnd f)) (LocalRecdefData.map f);
@@ -297,8 +285,6 @@
 (* setup theory *)
 
 val setup =
-  GlobalRecdefData.init #>
-  LocalRecdefData.init #>
   Attrib.add_attributes
    [(recdef_simpN, Attrib.add_del_args simp_add simp_del, "declaration of recdef simp rule"),
     (recdef_congN, Attrib.add_del_args cong_add cong_del, "declaration of recdef cong rule"),
diff -r 5f9138bcb3d7 -r fb79144af9a3 src/HOL/Tools/recfun_codegen.ML
--- a/src/HOL/Tools/recfun_codegen.ML	Sun May 06 21:50:17 2007 +0200
+++ b/src/HOL/Tools/recfun_codegen.ML	Mon May 07 00:49:59 2007 +0200
@@ -18,15 +18,13 @@
 open Codegen;
 
 structure RecCodegenData = TheoryDataFun
-(struct
-  val name = "HOL/recfun_codegen";
+(
   type T = (thm * string option) list Symtab.table;
   val empty = Symtab.empty;
   val copy = I;
   val extend = I;
   fun merge _ = Symtab.merge_list (Thm.eq_thm_prop o pairself fst);
-  fun print _ _ = ();
-end);
+);
 
 
 val dest_eqn = HOLogic.dest_eq o HOLogic.dest_Trueprop;
@@ -172,7 +170,6 @@
 
 
 val setup =
-  RecCodegenData.init #>
   add_codegen "recfun" recfun_codegen #>
   add_attribute ""
     (Args.del |-- Scan.succeed del
diff -r 5f9138bcb3d7 -r fb79144af9a3 src/HOL/Tools/record_package.ML
--- a/src/HOL/Tools/record_package.ML	Sun May 06 21:50:17 2007 +0200
+++ b/src/HOL/Tools/record_package.ML	Mon May 07 00:49:59 2007 +0200
@@ -243,7 +243,8 @@
 fun make_parent_info name fields extension induct =
  {name = name, fields = fields, extension = extension, induct = induct}: parent_info;
 
-(* data kind 'HOL/record' *)
+
+(* theory data *)
 
 type record_data =
  {records: record_info Symtab.table,
@@ -266,10 +267,8 @@
   extfields = extfields, fieldext = fieldext }: record_data;
 
 structure RecordsData = TheoryDataFun
-(struct
-  val name = "HOL/record"; 
+(
   type T = record_data;
-
   val empty =
     make_record_data Symtab.empty
       {selectors = Symtab.empty, updates = Symtab.empty, simpset = HOL_basic_ss}
@@ -308,27 +307,26 @@
                     (splits1, splits2))
       (Symtab.merge (K true) (extfields1,extfields2))
       (Symtab.merge (K true) (fieldext1,fieldext2));
+);
 
-  fun print thy ({records = recs, ...}: record_data) =
-    let
-      val prt_typ = Sign.pretty_typ thy;
-
-      fun pretty_parent NONE = []
-        | pretty_parent (SOME (Ts, name)) =
-            [Pretty.block [prt_typ (Type (name, Ts)), Pretty.str " +"]];
+fun print_records thy =
+  let
+    val {records = recs, ...} = RecordsData.get thy;
+    val prt_typ = Sign.pretty_typ thy;
 
-      fun pretty_field (c, T) = Pretty.block
-        [Pretty.str (Sign.extern_const thy c), Pretty.str " ::",
-          Pretty.brk 1, Pretty.quote (prt_typ T)];
+    fun pretty_parent NONE = []
+      | pretty_parent (SOME (Ts, name)) =
+          [Pretty.block [prt_typ (Type (name, Ts)), Pretty.str " +"]];
 
-      fun pretty_record (name, {args, parent, fields, ...}: record_info) =
-        Pretty.block (Pretty.fbreaks (Pretty.block
-          [prt_typ (Type (name, map TFree args)), Pretty.str " = "] ::
-          pretty_parent parent @ map pretty_field fields));
-    in map pretty_record (Symtab.dest recs) |> Pretty.chunks |> Pretty.writeln end;
-end);
+    fun pretty_field (c, T) = Pretty.block
+      [Pretty.str (Sign.extern_const thy c), Pretty.str " ::",
+        Pretty.brk 1, Pretty.quote (prt_typ T)];
 
-val print_records = RecordsData.print;
+    fun pretty_record (name, {args, parent, fields, ...}: record_info) =
+      Pretty.block (Pretty.fbreaks (Pretty.block
+        [prt_typ (Type (name, map TFree args)), Pretty.str " = "] ::
+        pretty_parent parent @ map pretty_field fields));
+  in map pretty_record (Symtab.dest recs) |> Pretty.chunks |> Pretty.writeln end;
 
 
 (* access 'records' *)
@@ -343,6 +341,7 @@
       sel_upd equalities extinjects extsplit splits extfields fieldext;
   in RecordsData.put data thy end;
 
+
 (* access 'sel_upd' *)
 
 val get_sel_upd = #sel_upd o RecordsData.get;
@@ -365,6 +364,7 @@
        equalities extinjects extsplit splits extfields fieldext;
   in RecordsData.put data thy end;
 
+
 (* access 'equalities' *)
 
 fun add_record_equalities name thm thy =
@@ -378,18 +378,21 @@
 
 val get_equalities =Symtab.lookup o #equalities o RecordsData.get;
 
+
 (* access 'extinjects' *)
 
 fun add_extinjects thm thy =
   let
     val {records, sel_upd, equalities, extinjects, extsplit, splits, extfields,fieldext} =
           RecordsData.get thy;
-    val data = make_record_data records sel_upd equalities (insert Thm.eq_thm_prop thm extinjects) extsplit
-                 splits extfields fieldext;
+    val data =
+      make_record_data records sel_upd equalities (insert Thm.eq_thm_prop thm extinjects) extsplit
+        splits extfields fieldext;
   in RecordsData.put data thy end;
 
 val get_extinjects = rev o #extinjects o RecordsData.get;
 
+
 (* access 'extsplit' *)
 
 fun add_extsplit name thm thy =
@@ -2263,7 +2266,6 @@
 (* setup theory *)
 
 val setup =
-  RecordsData.init #>
   Theory.add_trfuns ([], parse_translation, [], []) #>
   Theory.add_advanced_trfuns ([], adv_parse_translation, [], []) #>
   (fn thy => (Simplifier.change_simpset_of thy
diff -r 5f9138bcb3d7 -r fb79144af9a3 src/HOL/Tools/refute.ML
--- a/src/HOL/Tools/refute.ML	Sun May 06 21:50:17 2007 +0200
+++ b/src/HOL/Tools/refute.ML	Mon May 07 00:49:59 2007 +0200
@@ -186,9 +186,8 @@
     };
 
 
-  structure RefuteDataArgs =
-  struct
-    val name = "HOL/refute";
+  structure RefuteData = TheoryDataFun
+  (
     type T =
       {interpreters: (string * (theory -> model -> arguments -> Term.term ->
         (interpretation * model * arguments) option)) list,
@@ -204,15 +203,7 @@
       {interpreters = AList.merge (op =) (K true) (in1, in2),
        printers = AList.merge (op =) (K true) (pr1, pr2),
        parameters = Symtab.merge (op=) (pa1, pa2)};
-    fun print sg {interpreters, printers, parameters} =
-      Pretty.writeln (Pretty.chunks
-        [Pretty.strs ("default parameters:" :: List.concat (map
-          (fn (name, value) => [name, "=", value]) (Symtab.dest parameters))),
-         Pretty.strs ("interpreters:" :: map fst interpreters),
-         Pretty.strs ("printers:" :: map fst printers)]);
-  end;
-
-  structure RefuteData = TheoryDataFun(RefuteDataArgs);
+  );
 
 
 (* ------------------------------------------------------------------------- *)
@@ -3210,7 +3201,6 @@
   (* (theory -> theory) list *)
 
   val setup =
-     RefuteData.init #>
      add_interpreter "stlc"    stlc_interpreter #>
      add_interpreter "Pure"    Pure_interpreter #>
      add_interpreter "HOLogic" HOLogic_interpreter #>
diff -r 5f9138bcb3d7 -r fb79144af9a3 src/HOL/Tools/res_atpset.ML
--- a/src/HOL/Tools/res_atpset.ML	Sun May 06 21:50:17 2007 +0200
+++ b/src/HOL/Tools/res_atpset.ML	Mon May 07 00:49:59 2007 +0200
@@ -18,24 +18,22 @@
 
 structure Data = GenericDataFun
 (
-  val name = "HOL/atpset";
   type T = thm list;
   val empty = [];
   val extend = I;
   fun merge _ = Drule.merge_rules;
-  fun print context rules =
-    Pretty.writeln (Pretty.big_list "ATP rules:"
-      (map (ProofContext.pretty_thm (Context.proof_of context)) rules));
 );
 
-val print_atpset = Data.print o Context.Proof;
 val get_atpset = Data.get o Context.Proof;
 
+fun print_atpset ctxt =
+  Pretty.writeln (Pretty.big_list "ATP rules:"
+    (map (ProofContext.pretty_thm ctxt) (get_atpset ctxt)));
+
 val atp_add = Thm.declaration_attribute (Data.map o Drule.add_rule);
 val atp_del = Thm.declaration_attribute (Data.map o Drule.del_rule);
 
 val setup =
-  Data.init #>
   Attrib.add_attributes [("atp", Attrib.add_del_args atp_add atp_del, "declaration of ATP rules")];
 
 end;
diff -r 5f9138bcb3d7 -r fb79144af9a3 src/HOL/Tools/res_axioms.ML
--- a/src/HOL/Tools/res_axioms.ML	Sun May 06 21:50:17 2007 +0200
+++ b/src/HOL/Tools/res_axioms.ML	Mon May 07 00:49:59 2007 +0200
@@ -481,15 +481,13 @@
       (SOME (to_nnf th, fake_name th)  handle THM _ => NONE);
 
 structure ThmCache = TheoryDataFun
-(struct
-  val name = "ATP/thm_cache";
+(
   type T = (thm list) Thmtab.table ref;
   val empty : T = ref Thmtab.empty;
   fun copy (ref tab) : T = ref tab;
   val extend = copy;
   fun merge _ (ref tab1, ref tab2) : T = ref (Thmtab.merge (K true) (tab1, tab2));
-  fun print _ _ = ();
-end);
+);
 
 (*The cache prevents repeated clausification of a theorem, and also repeated declaration of 
   Skolem functions. The global one holds theorems proved prior to this point. Theory data
diff -r 5f9138bcb3d7 -r fb79144af9a3 src/HOL/Tools/typecopy_package.ML
--- a/src/HOL/Tools/typecopy_package.ML	Sun May 06 21:50:17 2007 +0200
+++ b/src/HOL/Tools/typecopy_package.ML	Mon May 07 00:49:59 2007 +0200
@@ -23,7 +23,7 @@
   val add_hook: hook -> theory -> theory
   val get_spec: theory -> string -> (string * sort) list * (string * typ list) list
   val get_eq: theory -> string -> thm
-  val print: theory -> unit
+  val print_typecopies: theory -> unit
   val setup: theory -> theory
 end;
 
@@ -44,33 +44,30 @@
 type hook = string * info -> theory -> theory;
 
 structure TypecopyData = TheoryDataFun
-(struct
-  val name = "HOL/typecopy_package";
+(
   type T = info Symtab.table * (serial * hook) list;
   val empty = (Symtab.empty, []);
   val copy = I;
   val extend = I;
   fun merge _ ((tab1, hooks1), (tab2, hooks2) : T) =
     (Symtab.merge (K true) (tab1, tab2), AList.merge (op =) (K true) (hooks1, hooks2));
-  fun print thy (tab, _) =
-    let
-      fun mk (tyco, { vs, constr, typ, proj = (proj, _), ... } : info) =
-        (Pretty.block o Pretty.breaks) [
-          Sign.pretty_typ thy (Type (tyco, map TFree vs)),
-          Pretty.str "=",
-          (Pretty.str o Sign.extern_const thy) constr,
-          Sign.pretty_typ thy typ,
-          Pretty.block [Pretty.str "(", (Pretty.str o Sign.extern_const thy) proj, Pretty.str  ")"]
-        ];
+);
+
+fun print_typecopies thy =
+  let
+    val (tab, _) = TypecopyData.get thy;
+    fun mk (tyco, { vs, constr, typ, proj = (proj, _), ... } : info) =
+      (Pretty.block o Pretty.breaks) [
+        Sign.pretty_typ thy (Type (tyco, map TFree vs)),
+        Pretty.str "=",
+        (Pretty.str o Sign.extern_const thy) constr,
+        Sign.pretty_typ thy typ,
+        Pretty.block [Pretty.str "(", (Pretty.str o Sign.extern_const thy) proj, Pretty.str  ")"]];
     in
-      (Pretty.writeln o Pretty.block o Pretty.fbreaks) (
-        Pretty.str "type copies:"
-        :: map mk (Symtab.dest tab)
-      )
+      (Pretty.writeln o Pretty.block o Pretty.fbreaks)
+        (Pretty.str "type copies:" :: map mk (Symtab.dest tab))
     end;
-end);
 
-val print = TypecopyData.print;
 val get_typecopies = Symtab.keys o fst o TypecopyData.get;
 val get_typecopy_info = Symtab.lookup o fst o TypecopyData.get;
 
@@ -128,7 +125,7 @@
 
 val add_typecopy = gen_add_typecopy Sign.certify_typ;
 
-end; (*local*)
+end;
 
 
 (* equality function equation and datatype specification *)
@@ -147,8 +144,6 @@
 fun add_project (_ , {proj_def, ...} : info) =
   CodegenData.add_func true proj_def;
 
-val setup =
-  TypecopyData.init
-  #> add_hook add_project;
+val setup = add_hook add_project;
 
-end; (*struct*)
+end;
diff -r 5f9138bcb3d7 -r fb79144af9a3 src/HOL/Tools/typedef_package.ML
--- a/src/HOL/Tools/typedef_package.ML	Sun May 06 21:50:17 2007 +0200
+++ b/src/HOL/Tools/typedef_package.ML	Mon May 07 00:49:59 2007 +0200
@@ -24,7 +24,6 @@
     * (string * string) option -> theory -> Proof.state
   val typedef_i: (bool * string) * (bstring * string list * mixfix) * term
     * (string * string) option -> theory -> Proof.state
-  val setup: theory -> theory
 end;
 
 structure TypedefPackage: TYPEDEF_PACKAGE =
@@ -77,15 +76,13 @@
   Abs_cases: thm, Rep_induct: thm, Abs_induct: thm};
 
 structure TypedefData = TheoryDataFun
-(struct
-  val name = "HOL/typedef";
+(
   type T = info Symtab.table;
   val empty = Symtab.empty;
   val copy = I;
   val extend = I;
   fun merge _ tabs : T = Symtab.merge (K true) tabs;
-  fun print _ _ = ();
-end);
+);
 
 val get_info = Symtab.lookup o TypedefData.get;
 fun put_info name info = TypedefData.map (Symtab.update (name, info));
@@ -270,8 +267,6 @@
 
 end;
 
-val setup = TypedefData.init;
-
 
 
 (** outer syntax **)
diff -r 5f9138bcb3d7 -r fb79144af9a3 src/HOL/Typedef.thy
--- a/src/HOL/Typedef.thy	Sun May 06 21:50:17 2007 +0200
+++ b/src/HOL/Typedef.thy	Mon May 07 00:49:59 2007 +0200
@@ -90,8 +90,7 @@
 use "Tools/typedef_codegen.ML"
 
 setup {*
-  TypedefPackage.setup
-  #> TypecopyPackage.setup
+  TypecopyPackage.setup
   #> TypedefCodegen.setup
 *}
 
diff -r 5f9138bcb3d7 -r fb79144af9a3 src/HOL/arith_data.ML
--- a/src/HOL/arith_data.ML	Sun May 06 21:50:17 2007 +0200
+++ b/src/HOL/arith_data.ML	Mon May 07 00:49:59 2007 +0200
@@ -206,8 +206,7 @@
 fun eq_arith_tactic (ArithTactic {id = id1, ...}, ArithTactic {id = id2, ...}) = (id1 = id2);
 
 structure ArithTheoryData = TheoryDataFun
-(struct
-  val name = "HOL/arith";
+(
   type T = {splits: thm list,
             inj_consts: (string * typ) list,
             discrete: string list,
@@ -221,8 +220,7 @@
     inj_consts = Library.merge (op =) (inj_consts1, inj_consts2),
     discrete = Library.merge (op =) (discrete1, discrete2),
     tactics = Library.merge eq_arith_tactic (tactics1, tactics2)};
-  fun print _ _ = ();
-end);
+);
 
 val arith_split_add = Thm.declaration_attribute (fn thm =>
   Context.mapping (ArithTheoryData.map (fn {splits,inj_consts,discrete,tactics} =>
@@ -922,7 +920,6 @@
    Most of the work is done by the cancel tactics. *)
 
 val init_lin_arith_data =
- Fast_Arith.setup #>
  Fast_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, ...} =>
    {add_mono_thms = add_mono_thms @
     @{thms add_mono_thms_ordered_semiring} @ @{thms add_mono_thms_ordered_field},
@@ -940,7 +937,6 @@
       addsimprocs [ab_group_add_cancel.sum_conv, ab_group_add_cancel.rel_conv]
        (*abel_cancel helps it work in abstract algebraic domains*)
       addsimprocs nat_cancel_sums_add}) #>
-  ArithTheoryData.init #>
   arith_discrete "nat";
 
 val fast_nat_arith_simproc =
diff -r 5f9138bcb3d7 -r fb79144af9a3 src/Provers/Arith/fast_lin_arith.ML
--- a/src/Provers/Arith/fast_lin_arith.ML	Sun May 06 21:50:17 2007 +0200
+++ b/src/Provers/Arith/fast_lin_arith.ML	Mon May 07 00:49:59 2007 +0200
@@ -86,7 +86,6 @@
 
 signature FAST_LIN_ARITH =
 sig
-  val setup: theory -> theory
   val map_data: ({add_mono_thms: thm list, mult_mono_thms: thm list, inj_thms: thm list,
                  lessD: thm list, neqE: thm list, simpset: Simplifier.simpset}
                  -> {add_mono_thms: thm list, mult_mono_thms: thm list, inj_thms: thm list,
@@ -99,18 +98,15 @@
   val cut_lin_arith_tac: simpset -> int -> tactic
 end;
 
-functor Fast_Lin_Arith(structure LA_Logic:LIN_ARITH_LOGIC 
+functor Fast_Lin_Arith(structure LA_Logic:LIN_ARITH_LOGIC
                        and       LA_Data:LIN_ARITH_DATA) : FAST_LIN_ARITH =
 struct
 
 
 (** theory data **)
 
-(* data kind 'Provers/fast_lin_arith' *)
-
 structure Data = TheoryDataFun
-(struct
-  val name = "Provers/fast_lin_arith";
+(
   type T = {add_mono_thms: thm list, mult_mono_thms: thm list, inj_thms: thm list,
             lessD: thm list, neqE: thm list, simpset: Simplifier.simpset};
 
@@ -130,12 +126,9 @@
      lessD = Drule.merge_rules (lessD1, lessD2),
      neqE = Drule.merge_rules (neqE1, neqE2),
      simpset = Simplifier.merge_ss (simpset1, simpset2)};
-
-  fun print _ _ = ();
-end);
+);
 
 val map_data = Data.map;
-val setup = Data.init;
 
 
 
@@ -424,7 +417,7 @@
 local
  exception FalseE of thm
 in
-fun mkthm (sg:theory, ss:simpset) (asms:thm list) (just:injust) : thm =
+fun mkthm (sg:theory, ss) (asms:thm list) (just:injust) : thm =
   let val {add_mono_thms, mult_mono_thms, inj_thms, lessD, simpset, ...} =
           Data.get sg;
       val simpset' = Simplifier.inherit_context ss simpset;
@@ -503,7 +496,7 @@
 fun integ(rlhs,r,rel,rrhs,s,d) =
 let val (rn,rd) = Rat.quotient_of_rat r and (sn,sd) = Rat.quotient_of_rat s
     val m = lcms(map (abs o snd o Rat.quotient_of_rat) (r :: s :: map snd rlhs @ map snd rrhs))
-    fun mult(t,r) = 
+    fun mult(t,r) =
         let val (i,j) = Rat.quotient_of_rat r
         in (t,i * (m div j)) end
 in (m,(map mult rlhs, rn*(m div rd), rel, map mult rrhs, sn*(m div sd), d)) end
@@ -527,7 +520,7 @@
                 else lineq(c,Lt,diff,just)
      | "~<"  => lineq(~c,Le,map (op~) diff,NotLessD(just))
      | "="   => lineq(c,Eq,diff,just)
-     | _     => sys_error("mklineq" ^ rel)   
+     | _     => sys_error("mklineq" ^ rel)
   end;
 
 (* ------------------------------------------------------------------------- *)
@@ -590,15 +583,9 @@
 (*        failure as soon as a case could not be refuted; i.e. delay further *)
 (*        splitting until after a refutation for other cases has been found. *)
 
-fun split_items sg (do_pre : bool) (Ts : typ list, terms : term list) :
+fun split_items sg (do_pre : bool) (Ts, terms) :
                 (typ list * (LA_Data.decompT * int) list) list =
 let
-(*
-  val _ = if !trace then
-            trace_msg ("split_items: Ts    = " ^ string_of_list (Sign.string_of_typ sg) Ts ^ "\n" ^
-                       "             terms = " ^ string_of_list (Sign.string_of_term sg) terms)
-          else ()
-*)
   (* splits inequalities '~=' into '<' and '>'; this corresponds to *)
   (* 'REPEAT_DETERM (eresolve_tac neqE i)' at the theorem/tactic    *)
   (* level                                                          *)
@@ -634,38 +621,14 @@
 
   val result = (Ts, terms)
     |> (* user-defined preprocessing of the subgoal *)
-       (* (typ list * term list) list *)
        (if do_pre then LA_Data.pre_decomp sg else Library.single)
-    |> (* compute the internal encoding of (in-)equalities *)
-       (* (typ list * (LA_Data.decompT option * bool) list) list *)
+    |> (* produce the internal encoding of (in-)equalities *)
        map (apsnd (map (fn t => (LA_Data.decomp sg t, LA_Data.domain_is_nat t))))
     |> (* splitting of inequalities *)
-       (* (typ list * (LA_Data.decompT option * bool) list list) list *)
        map (apsnd elim_neq)
-    |> (* combine the list of lists of subgoals into a single list *)
-       map (fn (Ts, subgoals) => map (pair Ts o map fst) subgoals)
-    |> List.concat
+    |> maps (fn (Ts, subgoals) => map (pair Ts o map fst) subgoals)
     |> (* numbering of hypotheses, ignoring irrelevant ones *)
        map (apsnd (number_hyps 0))
-(*
-  val _ = if !trace then
-            trace_msg ("split_items: result has " ^ Int.toString (length result) ^
-              " subgoal(s)" ^ "\n" ^ (cat_lines o fst) (fold_map (fn (Ts, items) => fn n =>
-                ("  " ^ Int.toString n ^ ". Ts    = " ^
-                   string_of_list (Sign.string_of_typ sg) Ts ^ "\n" ^
-                 "     items = " ^ string_of_list (string_of_pair 
-                   (fn (l, i, rel, r, j, d) => enclose "(" ")" (commas
-                     [string_of_list
-                        (string_of_pair (Sign.string_of_term sg) Rat.string_of_rat) l,
-                      Rat.string_of_rat i,
-                      rel,
-                      string_of_list
-                        (string_of_pair (Sign.string_of_term sg) Rat.string_of_rat) r,
-                      Rat.string_of_rat j,
-                      Bool.toString d]))
-                   Int.toString) items, n+1)) result 1))
-          else ()
-*)
 in result end;
 
 fun add_atoms (ats : term list, ((lhs,_,_,rhs,_,_) : LA_Data.decompT, _)) : term list =
@@ -742,7 +705,7 @@
       refute sg params show_ex do_pre Hs'
   end;
 
-fun refute_tac (ss : simpset) (i : int, justs : injust list) : tactic =
+fun refute_tac ss (i, justs) =
   fn state =>
     let val _ = trace_thm ("refute_tac (on subgoal " ^ Int.toString i ^ ", with " ^
                              Int.toString (length justs) ^ " justification(s)):") state
diff -r 5f9138bcb3d7 -r fb79144af9a3 src/Provers/classical.ML
--- a/src/Provers/classical.ML	Sun May 06 21:50:17 2007 +0200
+++ b/src/Provers/classical.ML	Mon May 07 00:49:59 2007 +0200
@@ -140,9 +140,9 @@
   val add_context_unsafe_wrapper: string * (Proof.context -> wrapper) -> theory -> theory
   val del_context_unsafe_wrapper: string -> theory -> theory
   val get_claset: theory -> claset
-  val print_local_claset: Proof.context -> unit
   val get_local_claset: Proof.context -> claset
   val put_local_claset: claset -> Proof.context -> Proof.context
+  val print_local_claset: Proof.context -> unit
   val safe_dest: int option -> attribute
   val safe_elim: int option -> attribute
   val safe_intro: int option -> attribute
@@ -857,19 +857,16 @@
 (* global claset *)
 
 structure GlobalClaset = TheoryDataFun
-(struct
-  val name = "Provers/claset";
+(
   type T = claset ref * context_cs;
-
   val empty = (ref empty_cs, empty_context_cs);
   fun copy (ref cs, ctxt_cs) = (ref cs, ctxt_cs): T;
   val extend = copy;
   fun merge _ ((ref cs1, ctxt_cs1), (ref cs2, ctxt_cs2)) =
     (ref (merge_cs (cs1, cs2)), merge_context_cs (ctxt_cs1, ctxt_cs2));
-  fun print _ (ref cs, _) = print_cs cs;
-end);
+);
 
-val print_claset = GlobalClaset.print;
+val print_claset = print_cs o ! o #1 o GlobalClaset.get;
 val get_claset = ! o #1 o GlobalClaset.get;
 
 val get_context_cs = #2 o GlobalClaset.get o ProofContext.theory_of;
@@ -912,20 +909,19 @@
 (* local claset *)
 
 structure LocalClaset = ProofDataFun
-(struct
-  val name = "Provers/claset";
+(
   type T = claset;
   val init = get_claset;
-  fun print ctxt cs = print_cs (context_cs ctxt cs (get_context_cs ctxt));
-end);
+);
 
-val print_local_claset = LocalClaset.print;
 val get_local_claset = LocalClaset.get;
 val put_local_claset = LocalClaset.put;
 
 fun local_claset_of ctxt =
   context_cs ctxt (get_local_claset ctxt) (get_context_cs ctxt);
 
+val print_local_claset = print_cs o local_claset_of;
+
 
 (* attributes *)
 
@@ -1061,7 +1057,7 @@
 
 (** theory setup **)
 
-val setup = GlobalClaset.init #> LocalClaset.init #> setup_attrs #> setup_methods;
+val setup = GlobalClaset.init #> setup_attrs #> setup_methods;
 
 
 
diff -r 5f9138bcb3d7 -r fb79144af9a3 src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Sun May 06 21:50:17 2007 +0200
+++ b/src/Pure/Isar/attrib.ML	Mon May 07 00:49:59 2007 +0200
@@ -49,29 +49,24 @@
 (* theory data *)
 
 structure AttributesData = TheoryDataFun
-(struct
-  val name = "Isar/attributes";
+(
   type T = (((src -> attribute) * string) * stamp) NameSpace.table;
-
   val empty = NameSpace.empty_table;
   val copy = I;
   val extend = I;
-
   fun merge _ tables = NameSpace.merge_tables (eq_snd (op =)) tables handle Symtab.DUPS dups =>
     error ("Attempt to merge different versions of attribute(s) " ^ commas_quote dups);
+);
 
-  fun print _ attribs =
-    let
-      fun prt_attr (name, ((_, comment), _)) = Pretty.block
-        [Pretty.str (name ^ ":"), Pretty.brk 2, Pretty.str comment];
-    in
-      [Pretty.big_list "attributes:" (map prt_attr (NameSpace.extern_table attribs))]
-      |> Pretty.chunks |> Pretty.writeln
-    end;
-end);
-
-val _ = Context.add_setup AttributesData.init;
-val print_attributes = AttributesData.print;
+fun print_attributes thy =
+  let
+    val attribs = AttributesData.get thy;
+    fun prt_attr (name, ((_, comment), _)) = Pretty.block
+      [Pretty.str (name ^ ":"), Pretty.brk 2, Pretty.str comment];
+  in
+    [Pretty.big_list "attributes:" (map prt_attr (NameSpace.extern_table attribs))]
+    |> Pretty.chunks |> Pretty.writeln
+  end;
 
 
 (* name space *)
diff -r 5f9138bcb3d7 -r fb79144af9a3 src/Pure/Isar/calculation.ML
--- a/src/Pure/Isar/calculation.ML	Sun May 06 21:50:17 2007 +0200
+++ b/src/Pure/Isar/calculation.ML	Mon May 07 00:49:59 2007 +0200
@@ -30,25 +30,21 @@
 
 structure CalculationData = GenericDataFun
 (
-  val name = "Isar/calculation";
   type T = (thm NetRules.T * thm list) * (thm list * int) option;
   val empty = ((NetRules.elim, []), NONE);
   val extend = I;
 
   fun merge _ (((trans1, sym1), _), ((trans2, sym2), _)) =
     ((NetRules.merge (trans1, trans2), Drule.merge_rules (sym1, sym2)), NONE);
-
-  fun print generic ((trans, sym), _) =
-    let val ctxt = Context.proof_of generic in
-      [Pretty.big_list "transitivity rules:"
-          (map (ProofContext.pretty_thm ctxt) (NetRules.rules trans)),
-        Pretty.big_list "symmetry rules:" (map (ProofContext.pretty_thm ctxt) sym)]
-      |> Pretty.chunks |> Pretty.writeln
-    end;
 );
 
-val _ = Context.add_setup CalculationData.init;
-val print_rules = CalculationData.print o Context.Proof;
+fun print_rules ctxt =
+  let val ((trans, sym), _) = CalculationData.get (Context.Proof ctxt) in
+    [Pretty.big_list "transitivity rules:"
+        (map (ProofContext.pretty_thm ctxt) (NetRules.rules trans)),
+      Pretty.big_list "symmetry rules:" (map (ProofContext.pretty_thm ctxt) sym)]
+    |> Pretty.chunks |> Pretty.writeln
+  end;
 
 
 (* access calculation *)
diff -r 5f9138bcb3d7 -r fb79144af9a3 src/Pure/Isar/context_rules.ML
--- a/src/Pure/Isar/context_rules.ML	Sun May 06 21:50:17 2007 +0200
+++ b/src/Pure/Isar/context_rules.ML	Mon May 07 00:49:59 2007 +0200
@@ -94,9 +94,7 @@
 
 structure Rules = GenericDataFun
 (
-  val name = "Pure/rules";
   type T = T;
-
   val empty = make_rules ~1 [] empty_netpairs ([], []);
   val extend = I;
 
@@ -112,20 +110,17 @@
           nth_map i (curry insert_tagged_brl ((w, n), (b, th))))
         (next upto ~1 ~~ rules) empty_netpairs;
     in make_rules (next - 1) rules netpairs wrappers end
-
-  fun print generic (Rules {rules, ...}) =
-    let
-      val ctxt = Context.proof_of generic;
-      fun prt_kind (i, b) =
-        Pretty.big_list ((the o AList.lookup (op =) kind_names) (i, b) ^ ":")
-          (map_filter (fn (_, (k, th)) =>
-              if k = (i, b) then SOME (ProofContext.pretty_thm ctxt th) else NONE)
-            (sort (int_ord o pairself fst) rules));
-    in Pretty.writeln (Pretty.chunks (map prt_kind rule_kinds)) end;
 );
 
-val _ = Context.add_setup Rules.init;
-val print_rules = Rules.print o Context.Proof;
+fun print_rules ctxt =
+  let
+    val Rules {rules, ...} = Rules.get (Context.Proof ctxt);
+    fun prt_kind (i, b) =
+      Pretty.big_list ((the o AList.lookup (op =) kind_names) (i, b) ^ ":")
+        (map_filter (fn (_, (k, th)) =>
+            if k = (i, b) then SOME (ProofContext.pretty_thm ctxt th) else NONE)
+          (sort (int_ord o pairself fst) rules));
+  in Pretty.writeln (Pretty.chunks (map prt_kind rule_kinds)) end;
 
 
 (* access data *)
diff -r 5f9138bcb3d7 -r fb79144af9a3 src/Pure/Isar/induct_attrib.ML
--- a/src/Pure/Isar/induct_attrib.ML	Sun May 06 21:50:17 2007 +0200
+++ b/src/Pure/Isar/induct_attrib.ML	Mon May 07 00:49:59 2007 +0200
@@ -94,49 +94,43 @@
 
 (* context data *)
 
-fun dest ((casesT, casesS), (inductT, inductS), (coinductT, coinductS)) =
-  {type_cases = NetRules.rules casesT,
-   set_cases = NetRules.rules casesS,
-   type_induct = NetRules.rules inductT,
-   set_induct = NetRules.rules inductS,
-   type_coinduct = NetRules.rules coinductT,
-   set_coinduct = NetRules.rules coinductS};
-
 structure Induct = GenericDataFun
 (
-  val name = "Isar/induct";
   type T = (rules * rules) * (rules * rules) * (rules * rules);
-
   val empty =
     ((init_rules (left_var_prem o #2), init_rules (Thm.major_prem_of o #2)),
      (init_rules (right_var_concl o #2), init_rules (Thm.major_prem_of o #2)),
      (init_rules (left_var_concl o #2), init_rules (Thm.concl_of o #2)));
-
   val extend = I;
-
   fun merge _ (((casesT1, casesS1), (inductT1, inductS1), (coinductT1, coinductS1)),
       ((casesT2, casesS2), (inductT2, inductS2), (coinductT2, coinductS2))) =
     ((NetRules.merge (casesT1, casesT2), NetRules.merge (casesS1, casesS2)),
       (NetRules.merge (inductT1, inductT2), NetRules.merge (inductS1, inductS2)),
       (NetRules.merge (coinductT1, coinductT2), NetRules.merge (coinductS1, coinductS2)));
-
-  fun print generic ((casesT, casesS), (inductT, inductS), (coinductT, coinductS)) =
-    let val ctxt = Context.proof_of generic in
-     [pretty_rules ctxt "coinduct type:" coinductT,
-      pretty_rules ctxt "coinduct set:" coinductS,
-      pretty_rules ctxt "induct type:" inductT,
-      pretty_rules ctxt "induct set:" inductS,
-      pretty_rules ctxt "cases type:" casesT,
-      pretty_rules ctxt "cases set:" casesS]
-     |> Pretty.chunks |> Pretty.writeln
-    end
 );
 
-val _ = Context.add_setup Induct.init;
-val print_rules = Induct.print o Context.Proof;
-val dest_rules = dest o Induct.get o Context.Proof;
+val get_local = Induct.get o Context.Proof;
 
-val get_local = Induct.get o Context.Proof;
+fun dest_rules ctxt =
+  let val ((casesT, casesS), (inductT, inductS), (coinductT, coinductS)) = get_local ctxt in
+    {type_cases = NetRules.rules casesT,
+     set_cases = NetRules.rules casesS,
+     type_induct = NetRules.rules inductT,
+     set_induct = NetRules.rules inductS,
+     type_coinduct = NetRules.rules coinductT,
+     set_coinduct = NetRules.rules coinductS}
+  end;
+
+fun print_rules ctxt =
+  let val ((casesT, casesS), (inductT, inductS), (coinductT, coinductS)) = get_local ctxt in
+   [pretty_rules ctxt "coinduct type:" coinductT,
+    pretty_rules ctxt "coinduct set:" coinductS,
+    pretty_rules ctxt "induct type:" inductT,
+    pretty_rules ctxt "induct set:" inductS,
+    pretty_rules ctxt "cases type:" casesT,
+    pretty_rules ctxt "cases set:" casesS]
+    |> Pretty.chunks |> Pretty.writeln
+  end;
 
 
 (* access rules *)
diff -r 5f9138bcb3d7 -r fb79144af9a3 src/Pure/Isar/local_defs.ML
--- a/src/Pure/Isar/local_defs.ML	Sun May 06 21:50:17 2007 +0200
+++ b/src/Pure/Isar/local_defs.ML	Mon May 07 00:49:59 2007 +0200
@@ -147,19 +147,15 @@
 
 structure Rules = GenericDataFun
 (
-  val name = "Pure/derived_defs";
   type T = thm list;
   val empty = []
   val extend = I;
   fun merge _ = Drule.merge_rules;
-  fun print context rules =
-    Pretty.writeln (Pretty.big_list "definitional transformations:"
-      (map (ProofContext.pretty_thm (Context.proof_of context)) rules));
 );
 
-val _ = Context.add_setup Rules.init;
-
-val print_rules = Rules.print o Context.Proof;
+fun print_rules ctxt =
+  Pretty.writeln (Pretty.big_list "definitional transformations:"
+    (map (ProofContext.pretty_thm ctxt) (Rules.get (Context.Proof ctxt))));
 
 val defn_add = Thm.declaration_attribute (Rules.map o Drule.add_rule);
 val defn_del = Thm.declaration_attribute (Rules.map o Drule.del_rule);
diff -r 5f9138bcb3d7 -r fb79144af9a3 src/Pure/Isar/local_theory.ML
--- a/src/Pure/Isar/local_theory.ML	Sun May 06 21:50:17 2007 +0200
+++ b/src/Pure/Isar/local_theory.ML	Mon May 07 00:49:59 2007 +0200
@@ -88,12 +88,9 @@
 
 structure Data = ProofDataFun
 (
-  val name = "Pure/local_theory";
   type T = lthy option;
   fun init _ = NONE;
-  fun print _ _ = ();
 );
-val _ = Context.add_setup Data.init;
 
 fun get_lthy lthy =
   (case Data.get lthy of
diff -r 5f9138bcb3d7 -r fb79144af9a3 src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Sun May 06 21:50:17 2007 +0200
+++ b/src/Pure/Isar/locale.ML	Mon May 07 00:49:59 2007 +0200
@@ -305,8 +305,7 @@
 (** theory data **)
 
 structure GlobalLocalesData = TheoryDataFun
-(struct
-  val name = "Isar/locales";
+(
   type T = NameSpace.T * locale Symtab.table * Registrations.T Symtab.table;
     (* 1st entry: locale namespace,
        2nd entry: locales of the theory,
@@ -332,33 +331,26 @@
   fun merge _ ((space1, locs1, regs1), (space2, locs2, regs2)) =
     (NameSpace.merge (space1, space2), Symtab.join join_locales (locs1, locs2),
      Symtab.join (K Registrations.join) (regs1, regs2));
-
-  fun print _ (space, locs, _) =
-    Pretty.strs ("locales:" :: map #1 (NameSpace.extern_table (space, locs)))
-    |> Pretty.writeln;
-end);
-
-val _ = Context.add_setup GlobalLocalesData.init;
+);
 
 
 
 (** context data **)
 
 structure LocalLocalesData = ProofDataFun
-(struct
-  val name = "Isar/locales";
-  type T = Registrations.T Symtab.table;
-    (* registrations, indexed by locale name *)
+(
+  type T = Registrations.T Symtab.table;  (*registrations, indexed by locale name*)
   fun init _ = Symtab.empty;
-  fun print _ _ = ();
-end);
-
-val _ = Context.add_setup LocalLocalesData.init;
+);
 
 
 (* access locales *)
 
-val print_locales = GlobalLocalesData.print;
+fun print_locales thy =
+  let val (space, locs, _) = GlobalLocalesData.get thy in
+    Pretty.strs ("locales:" :: map #1 (NameSpace.extern_table (space, locs)))
+    |> Pretty.writeln
+  end;
 
 val intern = NameSpace.intern o #1 o GlobalLocalesData.get;
 val extern = NameSpace.extern o #1 o GlobalLocalesData.get;
diff -r 5f9138bcb3d7 -r fb79144af9a3 src/Pure/Isar/method.ML
--- a/src/Pure/Isar/method.ML	Sun May 06 21:50:17 2007 +0200
+++ b/src/Pure/Isar/method.ML	Mon May 07 00:49:59 2007 +0200
@@ -378,28 +378,24 @@
 (* method definitions *)
 
 structure MethodsData = TheoryDataFun
-(struct
-  val name = "Isar/methods";
+(
   type T = (((src -> Proof.context -> method) * string) * stamp) NameSpace.table;
-
   val empty = NameSpace.empty_table;
   val copy = I;
   val extend = I;
   fun merge _ tables = NameSpace.merge_tables (eq_snd (op =)) tables handle Symtab.DUPS dups =>
     error ("Attempt to merge different versions of method(s) " ^ commas_quote dups);
+);
 
-  fun print _ meths =
-    let
-      fun prt_meth (name, ((_, comment), _)) = Pretty.block
-        [Pretty.str (name ^ ":"), Pretty.brk 2, Pretty.str comment];
-    in
-      [Pretty.big_list "methods:" (map prt_meth (NameSpace.extern_table meths))]
-      |> Pretty.chunks |> Pretty.writeln
-    end;
-end);
-
-val _ = Context.add_setup MethodsData.init;
-val print_methods = MethodsData.print;
+fun print_methods thy =
+  let
+    val meths = MethodsData.get thy;
+    fun prt_meth (name, ((_, comment), _)) = Pretty.block
+      [Pretty.str (name ^ ":"), Pretty.brk 2, Pretty.str comment];
+  in
+    [Pretty.big_list "methods:" (map prt_meth (NameSpace.extern_table meths))]
+    |> Pretty.chunks |> Pretty.writeln
+  end;
 
 
 (* get methods *)
diff -r 5f9138bcb3d7 -r fb79144af9a3 src/Pure/Isar/object_logic.ML
--- a/src/Pure/Isar/object_logic.ML	Sun May 06 21:50:17 2007 +0200
+++ b/src/Pure/Isar/object_logic.ML	Mon May 07 00:49:59 2007 +0200
@@ -38,11 +38,9 @@
 (** theory data **)
 
 structure ObjectLogicData = TheoryDataFun
-(struct
-  val name = "Pure/object_logic";
+(
   type T = string option * (thm list * thm list);
-
-  val empty = (NONE, ([], [Drule.norm_hhf_eq]));
+  val empty = (NONE, ([], []));
   val copy = I;
   val extend = I;
 
@@ -53,11 +51,7 @@
   fun merge _ ((judgment1, (atomize1, rulify1)), (judgment2, (atomize2, rulify2))) =
     (merge_judgment (judgment1, judgment2),
       (Drule.merge_rules (atomize1, atomize2), Drule.merge_rules (rulify1, rulify2)));
-
-  fun print _ _ = ();
-end);
-
-val _ = Context.add_setup ObjectLogicData.init;
+);
 
 
 
@@ -136,11 +130,13 @@
 val get_atomize = #1 o #2 o ObjectLogicData.get;
 val get_rulify = #2 o #2 o ObjectLogicData.get;
 
-val declare_atomize = Thm.declaration_attribute (fn th =>
-  Context.mapping (ObjectLogicData.map (apsnd (apfst (Drule.add_rule th)))) I);
+val add_atomize = ObjectLogicData.map o apsnd o apfst o Drule.add_rule;
+val add_rulify = ObjectLogicData.map o apsnd o apsnd o Drule.add_rule;
 
-val declare_rulify = Thm.declaration_attribute (fn th =>
-  Context.mapping (ObjectLogicData.map (apsnd (apsnd (Drule.add_rule th)))) I);
+val declare_atomize = Thm.declaration_attribute (fn th => Context.mapping (add_atomize th) I);
+val declare_rulify = Thm.declaration_attribute (fn th => Context.mapping (add_rulify th) I);
+
+val _ = Context.add_setup (add_rulify Drule.norm_hhf_eq);
 
 
 (* atomize *)
diff -r 5f9138bcb3d7 -r fb79144af9a3 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Sun May 06 21:50:17 2007 +0200
+++ b/src/Pure/Isar/proof_context.ML	Mon May 07 00:49:59 2007 +0200
@@ -198,17 +198,13 @@
 
 structure ContextData = ProofDataFun
 (
-  val name = "Isar/context";
   type T = ctxt;
   fun init thy =
     make_ctxt (false, local_naming, LocalSyntax.init thy,
       (Sign.consts_of thy, Sign.consts_of thy),
       (NameSpace.empty_table, FactIndex.empty), []);
-  fun print _ _ = ();
 );
 
-val _ = Context.add_setup ContextData.init;
-
 fun rep_context ctxt = ContextData.get ctxt |> (fn Ctxt args => args);
 
 fun map_context f =
diff -r 5f9138bcb3d7 -r fb79144af9a3 src/Pure/Isar/theory_target.ML
--- a/src/Pure/Isar/theory_target.ML	Sun May 06 21:50:17 2007 +0200
+++ b/src/Pure/Isar/theory_target.ML	Mon May 07 00:49:59 2007 +0200
@@ -22,13 +22,10 @@
 
 structure Data = ProofDataFun
 (
-  val name = "Isar/theory_target";
   type T = string option;
   fun init _ = NONE;
-  fun print _ _ = ();
 );
 
-val _ = Context.add_setup Data.init;
 val peek = Data.get;
 
 
diff -r 5f9138bcb3d7 -r fb79144af9a3 src/Pure/Proof/extraction.ML
--- a/src/Pure/Proof/extraction.ML	Sun May 06 21:50:17 2007 +0200
+++ b/src/Pure/Proof/extraction.ML	Mon May 07 00:49:59 2007 +0200
@@ -171,11 +171,10 @@
 
 (**** theory data ****)
 
-(* data kind 'Pure/extraction' *)
+(* theory data *)
 
 structure ExtractionData = TheoryDataFun
-(struct
-  val name = "Pure/extraction";
+(
   type T =
     {realizes_eqns : rules,
      typeof_eqns : rules,
@@ -209,11 +208,7 @@
      defs = Library.merge Thm.eq_thm (defs1, defs2),
      expand = Library.merge (op =) (expand1, expand2),
      prep = (case prep1 of NONE => prep2 | _ => prep1)};
-
-  fun print _ _ = ();
-end);
-
-val _ = Context.add_setup ExtractionData.init;
+);
 
 fun read_condeq thy =
   let val thy' = add_syntax thy
diff -r 5f9138bcb3d7 -r fb79144af9a3 src/Pure/Thy/present.ML
--- a/src/Pure/Thy/present.ML	Sun May 06 21:50:17 2007 +0200
+++ b/src/Pure/Thy/present.ML	Mon May 07 00:49:59 2007 +0200
@@ -75,17 +75,13 @@
 (** additional theory data **)
 
 structure BrowserInfoData = TheoryDataFun
-(struct
-  val name = "Pure/browser_info";
+(
   type T = {name: string, session: string list, is_local: bool};
   val empty = {name = "", session = [], is_local = false}: T;
   val copy = I;
   fun extend _ = empty;
   fun merge _ _ = empty;
-  fun print _ _ = ();
-end);
-
-val _ = Context.add_setup BrowserInfoData.init;
+);
 
 fun get_info thy =
   if member (op =) [Context.ProtoPureN, Context.PureN, Context.CPureN] (Context.theory_name thy)
diff -r 5f9138bcb3d7 -r fb79144af9a3 src/Pure/Thy/term_style.ML
--- a/src/Pure/Thy/term_style.ML	Sun May 06 21:50:17 2007 +0200
+++ b/src/Pure/Thy/term_style.ML	Mon May 07 00:49:59 2007 +0200
@@ -22,19 +22,17 @@
   error ("Duplicate declaration of antiquote style(s): " ^ commas_quote names);
 
 structure StyleData = TheoryDataFun
-(struct
-  val name = "Isar/antiquote_style";
+(
   type T = ((Proof.context -> term -> term) * stamp) Symtab.table;
   val empty = Symtab.empty;
   val copy = I;
   val extend = I;
   fun merge _ tabs = Symtab.merge (eq_snd (op =)) tabs
     handle Symtab.DUPS dups => err_dup_styles dups;
-  fun print _ tab = Pretty.writeln (Pretty.strs ("antiquote styles:" :: Symtab.keys tab));
-end);
+);
 
-val _ = Context.add_setup StyleData.init;
-val print_styles = StyleData.print;
+fun print_styles thy =
+  Pretty.writeln (Pretty.strs ("antiquote styles:" :: Symtab.keys (StyleData.get thy)));
 
 
 (* accessors *)
diff -r 5f9138bcb3d7 -r fb79144af9a3 src/Pure/Tools/class_package.ML
--- a/src/Pure/Tools/class_package.ML	Sun May 06 21:50:17 2007 +0200
+++ b/src/Pure/Tools/class_package.ML	Mon May 07 00:49:59 2007 +0200
@@ -237,20 +237,15 @@
 
 fun merge_pair f1 f2 ((x1, y1), (x2, y2)) = (f1 (x1, x2), f2 (y1, y2));
 
-structure ClassData = TheoryDataFun (
-  struct
-    val name = "Pure/classes";
-    type T = class_data Graph.T * class Symtab.table (*locale name ~> class name*);
-    val empty = (Graph.empty, Symtab.empty);
-    val copy = I;
-    val extend = I;
-    fun merge _ = merge_pair (Graph.merge (K true)) (Symtab.merge (K true));
-    fun print _ _ = ();
-  end
+structure ClassData = TheoryDataFun
+(
+  type T = class_data Graph.T * class Symtab.table (*locale name ~> class name*);
+  val empty = (Graph.empty, Symtab.empty);
+  val copy = I;
+  val extend = I;
+  fun merge _ = merge_pair (Graph.merge (K true)) (Symtab.merge (K true));
 );
 
-val _ = Context.add_setup ClassData.init;
-
 
 (* queries *)
 
diff -r 5f9138bcb3d7 -r fb79144af9a3 src/Pure/Tools/codegen_data.ML
--- a/src/Pure/Tools/codegen_data.ML	Sun May 06 21:50:17 2007 +0200
+++ b/src/Pure/Tools/codegen_data.ML	Mon May 07 00:49:59 2007 +0200
@@ -312,8 +312,7 @@
 type data = Object.T Datatab.table;
 
 structure CodeData = TheoryDataFun
-(struct
-  val name = "Pure/codegen_data";
+(
   type T = exec * data ref;
   val empty = (empty_exec, ref Datatab.empty : data ref);
   fun copy (exec, data) = (exec, ref (! data));
@@ -325,67 +324,67 @@
       val data2' = Datatab.map' (invoke_purge NONE touched) (! data2);
       val data = Datatab.join (invoke_merge pp) (data1', data2');
     in (exec, ref data) end;
-  fun print thy (exec, _) =
-    let
-      val ctxt = ProofContext.init thy;
-      fun pretty_func (s, lthms) =
-        (Pretty.block o Pretty.fbreaks) (
-          Pretty.str s :: pretty_sdthms ctxt lthms
-        );
-      fun pretty_dtyp (s, []) =
+);
+
+fun print_codesetup thy =
+  let
+    val ctxt = ProofContext.init thy;
+    val (exec, _) = CodeData.get thy;
+    fun pretty_func (s, lthms) =
+      (Pretty.block o Pretty.fbreaks) (
+        Pretty.str s :: pretty_sdthms ctxt lthms
+      );
+    fun pretty_dtyp (s, []) =
+          Pretty.str s
+      | pretty_dtyp (s, cos) =
+          (Pretty.block o Pretty.breaks) (
             Pretty.str s
-        | pretty_dtyp (s, cos) =
-            (Pretty.block o Pretty.breaks) (
-              Pretty.str s
-              :: Pretty.str "="
-              :: separate (Pretty.str "|") (map (fn (c, []) => Pretty.str c
-                   | (c, tys) =>
-                       (Pretty.block o Pretty.breaks)
-                          (Pretty.str c :: Pretty.str "of" :: map (Pretty.quote o Sign.pretty_typ thy) tys)) cos)
-            );
-      val inlines = (#inlines o the_preproc) exec;
-      val inline_procs = (map fst o #inline_procs o the_preproc) exec;
-      val preprocs = (map fst o #preprocs o the_preproc) exec;
-      val funs = the_funcs exec
-        |> Consttab.dest
-        |> (map o apfst) (CodegenConsts.string_of_const thy)
-        |> sort (string_ord o pairself fst);
-      val dtyps = the_dtyps exec
-        |> Symtab.dest
-        |> map (fn (dtco, (vs, cos)) => (Sign.string_of_typ thy (Type (dtco, map TFree vs)), cos))
-        |> sort (string_ord o pairself fst)
-    in
-      (Pretty.writeln o Pretty.chunks) [
-        Pretty.block (
-          Pretty.str "defining equations:"
-          :: Pretty.fbrk
-          :: (Pretty.fbreaks o map pretty_func) funs
-        ),
-        Pretty.block (
-          Pretty.str "inlining theorems:"
-          :: Pretty.fbrk
-          :: (Pretty.fbreaks o map (ProofContext.pretty_thm ctxt)) inlines
-        ),
-        Pretty.block (
-          Pretty.str "inlining procedures:"
-          :: Pretty.fbrk
-          :: (Pretty.fbreaks o map Pretty.str) inline_procs
-        ),
-        Pretty.block (
-          Pretty.str "preprocessors:"
-          :: Pretty.fbrk
-          :: (Pretty.fbreaks o map Pretty.str) preprocs
-        ),
-        Pretty.block (
-          Pretty.str "datatypes:"
-          :: Pretty.fbrk
-          :: (Pretty.fbreaks o map pretty_dtyp) dtyps
-        )
-      ]
-    end;
-end);
-
-val print_codesetup = CodeData.print;
+            :: Pretty.str "="
+            :: separate (Pretty.str "|") (map (fn (c, []) => Pretty.str c
+                 | (c, tys) =>
+                     (Pretty.block o Pretty.breaks)
+                        (Pretty.str c :: Pretty.str "of" :: map (Pretty.quote o Sign.pretty_typ thy) tys)) cos)
+          );
+    val inlines = (#inlines o the_preproc) exec;
+    val inline_procs = (map fst o #inline_procs o the_preproc) exec;
+    val preprocs = (map fst o #preprocs o the_preproc) exec;
+    val funs = the_funcs exec
+      |> Consttab.dest
+      |> (map o apfst) (CodegenConsts.string_of_const thy)
+      |> sort (string_ord o pairself fst);
+    val dtyps = the_dtyps exec
+      |> Symtab.dest
+      |> map (fn (dtco, (vs, cos)) => (Sign.string_of_typ thy (Type (dtco, map TFree vs)), cos))
+      |> sort (string_ord o pairself fst)
+  in
+    (Pretty.writeln o Pretty.chunks) [
+      Pretty.block (
+        Pretty.str "defining equations:"
+        :: Pretty.fbrk
+        :: (Pretty.fbreaks o map pretty_func) funs
+      ),
+      Pretty.block (
+        Pretty.str "inlining theorems:"
+        :: Pretty.fbrk
+        :: (Pretty.fbreaks o map (ProofContext.pretty_thm ctxt)) inlines
+      ),
+      Pretty.block (
+        Pretty.str "inlining procedures:"
+        :: Pretty.fbrk
+        :: (Pretty.fbreaks o map Pretty.str) inline_procs
+      ),
+      Pretty.block (
+        Pretty.str "preprocessors:"
+        :: Pretty.fbrk
+        :: (Pretty.fbreaks o map Pretty.str) preprocs
+      ),
+      Pretty.block (
+        Pretty.str "datatypes:"
+        :: Pretty.fbrk
+        :: (Pretty.fbreaks o map pretty_dtyp) dtyps
+      )
+    ]
+  end;
 
 fun init k = CodeData.map
   (fn (exec, data) => (exec, ref (Datatab.update (k, invoke_empty k) (! data))));
diff -r 5f9138bcb3d7 -r fb79144af9a3 src/Pure/Tools/codegen_names.ML
--- a/src/Pure/Tools/codegen_names.ML	Sun May 06 21:50:17 2007 +0200
+++ b/src/Pure/Tools/codegen_names.ML	Mon May 07 00:49:59 2007 +0200
@@ -292,18 +292,16 @@
 end; (*local*)
 
 structure CodeName = TheoryDataFun
-(struct
-  val name = "Pure/codegen_names";
+(
   type T = names ref;
   val empty = ref empty_names;
   fun copy (ref names) = ref names;
   val extend = copy;
   fun merge _ (ref names1, ref names2) = ref (merge_names (names1, names2));
-  fun print _ _ = ();
-end);
+);
 
 structure ConstName = CodeDataFun
-(struct
+(
   val name = "Pure/codegen_names";
   type T = const Consttab.table * (string * string option) Symtab.table;
   val empty = (Consttab.empty, Symtab.empty);
@@ -313,7 +311,7 @@
   fun purge _ NONE _ = empty
     | purge _ (SOME cs) (const, constrev) = (fold Consttab.delete_safe cs const,
         fold Symtab.delete (map_filter (Consttab.lookup const) cs) constrev);
-end);
+);
 
 val _ = Context.add_setup (CodeName.init #> ConstName.init);
 
diff -r 5f9138bcb3d7 -r fb79144af9a3 src/Pure/Tools/codegen_package.ML
--- a/src/Pure/Tools/codegen_package.ML	Sun May 06 21:50:17 2007 +0200
+++ b/src/Pure/Tools/codegen_package.ML	Mon May 07 00:49:59 2007 +0200
@@ -51,18 +51,17 @@
     Consttab.merge CodegenConsts.eq_const (consts1, consts2));
 
 structure CodegenPackageData = TheoryDataFun
-(struct
-  val name = "Pure/codegen_package_setup";
+(
   type T = appgens * abstypes;
   val empty = (Symtab.empty, (Symtab.empty, Consttab.empty));
   val copy = I;
   val extend = I;
   fun merge _ ((appgens1, abstypes1), (appgens2, abstypes2)) =
     (merge_appgens (appgens1, appgens2), merge_abstypes (abstypes1, abstypes2));
-  fun print _ _ = ();
-end);
+);
 
-structure Funcgr = CodegenFuncgrRetrieval (
+structure Funcgr = CodegenFuncgrRetrieval
+(
   val name = "Pure/codegen_package_thms";
   fun rewrites thy = [];
 );
@@ -94,7 +93,7 @@
   in Present.display_graph prgr end;
 
 structure Code = CodeDataFun
-(struct
+(
   val name = "Pure/codegen_package_code";
   type T = CodegenThingol.code;
   val empty = CodegenThingol.empty_code;
@@ -110,9 +109,9 @@
               o filter (member CodegenConsts.eq_const cs_exisiting)
             ) cs;
         in Graph.del_nodes dels code end;
-end);
+);
 
-val _ = Context.add_setup (CodegenPackageData.init #> Funcgr.init #> Code.init);
+val _ = Context.add_setup (Funcgr.init #> Code.init);
 
 
 (* preparing defining equations *)
diff -r 5f9138bcb3d7 -r fb79144af9a3 src/Pure/Tools/codegen_serializer.ML
--- a/src/Pure/Tools/codegen_serializer.ML	Sun May 06 21:50:17 2007 +0200
+++ b/src/Pure/Tools/codegen_serializer.ML	Mon May 07 00:49:59 2007 +0200
@@ -1539,15 +1539,13 @@
     error ("Incompatible serializers: " ^ quote target);
 
 structure CodegenSerializerData = TheoryDataFun
-(struct
-  val name = "Pure/codegen_serializer";
+(
   type T = target Symtab.table;
   val empty = Symtab.empty;
   val copy = I;
   val extend = I;
   fun merge _ = Symtab.join merge_target;
-  fun print _ _ = ();
-end);
+);
 
 fun the_serializer (Target { serializer, ... }) = serializer;
 fun the_reserved (Target { reserved, ... }) = reserved;
@@ -1587,8 +1585,7 @@
 val target_diag = "diag";
 
 val _ = Context.add_setup (
-  CodegenSerializerData.init
-  #> add_serializer (target_SML, isar_seri_sml)
+  add_serializer (target_SML, isar_seri_sml)
   #> add_serializer (target_OCaml, isar_seri_ocaml)
   #> add_serializer (target_Haskell, isar_seri_haskell)
   #> add_serializer (target_diag, (fn _ => fn _ => fn _ => seri_diagnosis))
diff -r 5f9138bcb3d7 -r fb79144af9a3 src/Pure/Tools/nbe.ML
--- a/src/Pure/Tools/nbe.ML	Sun May 06 21:50:17 2007 +0200
+++ b/src/Pure/Tools/nbe.ML	Mon May 07 00:49:59 2007 +0200
@@ -26,19 +26,14 @@
 (* preproc and postproc attributes *)
 
 structure NBE_Rewrite = TheoryDataFun
-(struct
-  val name = "Pure/nbe";
+(
   type T = thm list * thm list
-
-  val empty = ([],[])
+  val empty = ([], []);
   val copy = I;
   val extend = I;
-
   fun merge _ ((pres1,posts1), (pres2,posts2)) =
     (Library.merge Thm.eq_thm (pres1,pres2), Library.merge Thm.eq_thm (posts1,posts2))
-
-  fun print _ _ = ()
-end);
+);
 
 val _ =
   let
@@ -51,8 +46,7 @@
       || Args.$$$ "post" >> K attr_post));
   in
     Context.add_setup (
-      NBE_Rewrite.init
-      #> Attrib.add_attributes
+      Attrib.add_attributes
           [("normal", attr, "declare rewrite theorems for normalization")]
     )
   end;
diff -r 5f9138bcb3d7 -r fb79144af9a3 src/Pure/assumption.ML
--- a/src/Pure/assumption.ML	Sun May 06 21:50:17 2007 +0200
+++ b/src/Pure/assumption.ML	Mon May 07 00:49:59 2007 +0200
@@ -62,14 +62,10 @@
 
 structure Data = ProofDataFun
 (
-  val name = "Pure/assumption";
   type T = data;
   fun init _ = make_data ([], []);
-  fun print _ _ = ();
 );
 
-val _ = Context.add_setup Data.init;
-
 fun map_data f = Data.map (fn Data {assms, prems} => make_data (f (assms, prems)));
 fun rep_data ctxt = Data.get ctxt |> (fn Data args => args);
 
diff -r 5f9138bcb3d7 -r fb79144af9a3 src/Pure/axclass.ML
--- a/src/Pure/axclass.ML	Sun May 06 21:50:17 2007 +0200
+++ b/src/Pure/axclass.ML	Mon May 07 00:49:59 2007 +0200
@@ -95,18 +95,14 @@
 (* setup data *)
 
 structure AxClassData = TheoryDataFun
-(struct
-  val name = "Pure/axclass";
+(
   type T = axclasses * instances;
-  val empty : T = ((Symtab.empty, []), ([], Symtab.empty));
+  val empty = ((Symtab.empty, []), ([], Symtab.empty));
   val copy = I;
   val extend = I;
   fun merge pp ((axclasses1, instances1), (axclasses2, instances2)) =
     (merge_axclasses pp (axclasses1, axclasses2), (merge_instances (instances1, instances2)));
-  fun print _ _ = ();
-end);
-
-val _ = Context.add_setup AxClassData.init;
+);
 
 
 (* maintain axclasses *)
diff -r 5f9138bcb3d7 -r fb79144af9a3 src/Pure/codegen.ML
--- a/src/Pure/codegen.ML	Sun May 06 21:50:17 2007 +0200
+++ b/src/Pure/codegen.ML	Mon May 07 00:49:59 2007 +0200
@@ -199,13 +199,13 @@
   {size = size, iterations = iterations,
    default_type = SOME (Sign.read_typ thy s)};
 
-(* data kind 'Pure/codegen' *)
+
+(* theory data *)
 
 structure CodeData = CodegenData;
 
 structure CodegenData = TheoryDataFun
-(struct
-  val name = "Pure/codegen";
+(
   type T =
     {codegens : (string * term codegen) list,
      tycodegens : (string * typ codegen) list,
@@ -237,15 +237,15 @@
      preprocs = AList.merge (op =) (K true) (preprocs1, preprocs2),
      modules = Symtab.merge (K true) (modules1, modules2),
      test_params = merge_test_params test_params1 test_params2};
+);
 
-  fun print _ ({codegens, tycodegens, ...} : T) =
+fun print_codegens thy =
+  let val {codegens, tycodegens, ...} = CodegenData.get thy in
     Pretty.writeln (Pretty.chunks
       [Pretty.strs ("term code generators:" :: map fst codegens),
-       Pretty.strs ("type code generators:" :: map fst tycodegens)]);
-end);
+       Pretty.strs ("type code generators:" :: map fst tycodegens)])
+  end;
 
-val _ = Context.add_setup CodegenData.init;
-val print_codegens = CodegenData.print;
 
 
 (**** access parameters for random testing ****)
diff -r 5f9138bcb3d7 -r fb79144af9a3 src/Pure/compress.ML
--- a/src/Pure/compress.ML	Sun May 06 21:50:17 2007 +0200
+++ b/src/Pure/compress.ML	Mon May 07 00:49:59 2007 +0200
@@ -21,8 +21,7 @@
 (* theory data *)
 
 structure CompressData = TheoryDataFun
-(struct
-  val name = "Pure/compress";
+(
   type T = typ Typtab.table ref * term Termtab.table ref;
   val empty : T = (ref Typtab.empty, ref Termtab.empty);
   fun copy (ref typs, ref terms) : T = (ref typs, ref terms);
@@ -30,8 +29,7 @@
   fun merge _ ((ref typs1, ref terms1), (ref typs2, ref terms2)) : T =
    (ref (Typtab.merge (K true) (typs1, typs2)),
     ref (Termtab.merge (K true) (terms1, terms2)));
-  fun print _ _ = ();
-end);
+);
 
 val init_data = CompressData.init;
 
diff -r 5f9138bcb3d7 -r fb79144af9a3 src/Pure/display.ML
--- a/src/Pure/display.ML	Sun May 06 21:50:17 2007 +0200
+++ b/src/Pure/display.ML	Mon May 07 00:49:59 2007 +0200
@@ -234,9 +234,6 @@
     val rests = restricts |> map (apfst (apfst extern_const)) |> sort_wrt (#1 o #1);
   in
     [Pretty.strs ("names:" :: Context.names_of thy)] @
-    (if verbose then
-      [Pretty.strs ("theory data:" :: Context.theory_data_of thy),
-       Pretty.strs ("proof data:" :: Context.proof_data_of thy)] else []) @
     [Pretty.strs ["name prefix:", NameSpace.path_of naming],
       Pretty.big_list "classes:" (map pretty_classrel clsses),
       pretty_default default,
diff -r 5f9138bcb3d7 -r fb79144af9a3 src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Sun May 06 21:50:17 2007 +0200
+++ b/src/Pure/proofterm.ML	Mon May 07 00:49:59 2007 +0200
@@ -110,8 +110,6 @@
     (string * (typ list -> proof -> proof option)) list -> proof -> proof
   val rewrite_proof_notypes : (proof * proof) list *
     (string * (typ list -> proof -> proof option)) list -> proof -> proof
-  val init_data: theory -> theory
-
 end
 
 structure Proofterm : PROOFTERM =
@@ -1178,10 +1176,8 @@
 (**** theory data ****)
 
 structure ProofData = TheoryDataFun
-(struct
-  val name = "Pure/proof";
-  type T = ((proof * proof) list *
-    (string * (typ list -> proof -> proof option)) list);
+(
+  type T = (proof * proof) list * (string * (typ list -> proof -> proof option)) list;
 
   val empty = ([], []);
   val copy = I;
@@ -1189,10 +1185,7 @@
   fun merge _ ((rules1, procs1) : T, (rules2, procs2)) =
     (Library.merge (op =) (rules1, rules2),
       AList.merge (op =) (K true) (procs1, procs2));
-  fun print _ _ = ();
-end);
-
-val init_data = ProofData.init;
+);
 
 fun add_prf_rrule r = (ProofData.map o apfst) (insert (op =) r);
 
diff -r 5f9138bcb3d7 -r fb79144af9a3 src/Pure/pure_thy.ML
--- a/src/Pure/pure_thy.ML	Sun May 06 21:50:17 2007 +0200
+++ b/src/Pure/pure_thy.ML	Mon May 07 00:49:59 2007 +0200
@@ -152,7 +152,6 @@
 
 structure TheoremsData = TheoryDataFun
 (struct
-  val name = "Pure/theorems";
   type T =
    {theorems: thm list NameSpace.table,
     index: FactIndex.T} ref;
@@ -505,9 +504,6 @@
 val proto_pure =
   Context.pre_pure_thy
   |> Compress.init_data
-  |> Sign.init_data
-  |> Theory.init_data
-  |> Proofterm.init_data
   |> TheoremsData.init
   |> Sign.add_types
    [("fun", 2, NoSyn),
diff -r 5f9138bcb3d7 -r fb79144af9a3 src/Pure/sign.ML
--- a/src/Pure/sign.ML	Sun May 06 21:50:17 2007 +0200
+++ b/src/Pure/sign.ML	Mon May 07 00:49:59 2007 +0200
@@ -60,7 +60,6 @@
 
 signature SIGN =
 sig
-  val init_data: theory -> theory
   val rep_sg: theory ->
    {naming: NameSpace.naming,
     syn: Syntax.syntax,
@@ -203,8 +202,7 @@
   Sign {naming = naming, syn = syn, tsig = tsig, consts = consts};
 
 structure SignData = TheoryDataFun
-(struct
-  val name = "Pure/sign";
+(
   type T = sign;
   val copy = I;
   fun extend (Sign {syn, tsig, consts, ...}) =
@@ -223,11 +221,7 @@
       val tsig = Type.merge_tsigs pp (tsig1, tsig2);
       val consts = Consts.merge (consts1, consts2);
     in make_sign (naming, syn, tsig, consts) end;
-
-  fun print _ _ = ();
-end);
-
-val init_data = SignData.init;
+);
 
 fun rep_sg thy = SignData.get thy |> (fn Sign args => args);
 
diff -r 5f9138bcb3d7 -r fb79144af9a3 src/Pure/simplifier.ML
--- a/src/Pure/simplifier.ML	Sun May 06 21:50:17 2007 +0200
+++ b/src/Pure/simplifier.ML	Mon May 07 00:49:59 2007 +0200
@@ -97,19 +97,16 @@
 (* global simpsets *)
 
 structure GlobalSimpset = TheoryDataFun
-(struct
-  val name = "Pure/simpset";
+(
   type T = simpset ref;
-
   val empty = ref empty_ss;
-  fun copy (ref ss) = ref ss: T;            (*create new reference!*)
+  fun copy (ref ss) = ref ss: T;
   fun extend (ref ss) = ref (MetaSimplifier.inherit_context empty_ss ss);
   fun merge _ (ref ss1, ref ss2) = ref (merge_ss (ss1, ss2));
-  fun print _ (ref ss) = print_ss ss;
-end);
+);
 
 val _ = Context.add_setup GlobalSimpset.init;
-val print_simpset = GlobalSimpset.print;
+fun print_simpset thy = print_ss (! (GlobalSimpset.get thy));
 val get_simpset = ! o GlobalSimpset.get;
 
 val change_simpset_of = change o GlobalSimpset.get;
@@ -133,15 +130,12 @@
 (* local simpsets *)
 
 structure LocalSimpset = ProofDataFun
-(struct
-  val name = "Pure/simpset";
+(
   type T = simpset;
   val init = get_simpset;
-  fun print _ ss = print_ss ss;
-end);
+);
 
-val _ = Context.add_setup LocalSimpset.init;
-val print_local_simpset = LocalSimpset.print;
+val print_local_simpset = print_ss o LocalSimpset.get;
 val get_local_simpset = LocalSimpset.get;
 val put_local_simpset = LocalSimpset.put;
 
@@ -181,15 +175,12 @@
 
 structure Simprocs = GenericDataFun
 (
-  val name = "Pure/simprocs";
   type T = simproc NameSpace.table;
   val empty = NameSpace.empty_table;
   val extend = I;
   fun merge _ simprocs = NameSpace.merge_tables eq_simproc simprocs
     handle Symtab.DUPS ds => err_dup_simprocs ds;
-  fun print _ _ = ();
 );
-val _ = Context.add_setup Simprocs.init;
 
 
 (* get simprocs *)
diff -r 5f9138bcb3d7 -r fb79144af9a3 src/Pure/theory.ML
--- a/src/Pure/theory.ML	Sun May 06 21:50:17 2007 +0200
+++ b/src/Pure/theory.ML	Mon May 07 00:49:59 2007 +0200
@@ -21,7 +21,6 @@
   val end_theory: theory -> theory
   val checkpoint: theory -> theory
   val copy: theory -> theory
-  val init_data: theory -> theory
   val rep_theory: theory ->
    {axioms: term NameSpace.table,
     defs: Defs.T,
@@ -101,8 +100,7 @@
 fun err_dup_oras dups = error ("Duplicate oracle(s): " ^ commas_quote dups);
 
 structure ThyData = TheoryDataFun
-(struct
-  val name = "Pure/theory";
+(
   type T = thy;
   val empty = make_thy (NameSpace.empty_table, Defs.empty, NameSpace.empty_table);
   val copy = I;
@@ -119,11 +117,7 @@
       val oracles = NameSpace.merge_tables (eq_snd (op =)) (oracles1, oracles2)
         handle Symtab.DUPS dups => err_dup_oras dups;
     in make_thy (axioms, defs, oracles) end;
-
-  fun print _ _ = ();
-end);
-
-val init_data = ThyData.init;
+);
 
 fun rep_theory thy = ThyData.get thy |> (fn Thy args => args);
 
diff -r 5f9138bcb3d7 -r fb79144af9a3 src/Pure/variable.ML
--- a/src/Pure/variable.ML	Sun May 06 21:50:17 2007 +0200
+++ b/src/Pure/variable.ML	Mon May 07 00:49:59 2007 +0200
@@ -79,15 +79,11 @@
 
 structure Data = ProofDataFun
 (
-  val name = "Pure/variable";
   type T = data;
   fun init thy =
     make_data (false, Name.context, [], Vartab.empty, Symtab.empty, (Vartab.empty, Vartab.empty));
-  fun print _ _ = ();
 );
 
-val _ = Context.add_setup Data.init;
-
 fun map_data f =
   Data.map (fn Data {is_body, names, fixes, binds, type_occs, constraints} =>
     make_data (f (is_body, names, fixes, binds, type_occs, constraints)));
diff -r 5f9138bcb3d7 -r fb79144af9a3 src/ZF/Tools/ind_cases.ML
--- a/src/ZF/Tools/ind_cases.ML	Sun May 06 21:50:17 2007 +0200
+++ b/src/ZF/Tools/ind_cases.ML	Mon May 07 00:49:59 2007 +0200
@@ -19,16 +19,13 @@
 (* theory data *)
 
 structure IndCasesData = TheoryDataFun
-(struct
-  val name = "ZF/ind_cases";
+(
   type T = (simpset -> cterm -> thm) Symtab.table;
-
   val empty = Symtab.empty;
   val copy = I;
   val extend = I;
   fun merge _ tabs : T = Symtab.merge (K true) tabs;
-  fun print _ _ = ();
-end);
+);
 
 
 fun declare name f = IndCasesData.map (Symtab.update (name, f));
@@ -72,9 +69,8 @@
 (* package setup *)
 
 val setup =
- (IndCasesData.init #>
-  Method.add_methods [("ind_cases", mk_cases_meth oo mk_cases_args,
-    "dynamic case analysis on sets")]);
+  Method.add_methods
+    [("ind_cases", mk_cases_meth oo mk_cases_args, "dynamic case analysis on sets")];
 
 
 (* outer syntax *)
diff -r 5f9138bcb3d7 -r fb79144af9a3 src/ZF/Tools/induct_tacs.ML
--- a/src/ZF/Tools/induct_tacs.ML	Sun May 06 21:50:17 2007 +0200
+++ b/src/ZF/Tools/induct_tacs.ML	Mon May 07 00:49:59 2007 +0200
@@ -31,19 +31,14 @@
    exhaustion : thm};
 
 structure DatatypesData = TheoryDataFun
-(struct
-  val name = "ZF/datatypes";
+(
   type T = datatype_info Symtab.table;
-
   val empty = Symtab.empty;
   val copy = I;
   val extend = I;
   fun merge _ tabs : T = Symtab.merge (K true) tabs;
+);
 
-  fun print thy tab =
-    Pretty.writeln (Pretty.strs ("datatypes:" ::
-      map #1 (NameSpace.extern_table (Sign.type_space thy, tab))));
-end);
 
 
 (** Constructor information: needed to map constructors to datatypes **)
@@ -56,15 +51,13 @@
 
 
 structure ConstructorsData = TheoryDataFun
-(struct
-  val name = "ZF/constructors"
+(
   type T = constructor_info Symtab.table
   val empty = Symtab.empty
   val copy = I;
   val extend = I
   fun merge _ tabs: T = Symtab.merge (K true) tabs;
-  fun print _ _= ();
-end);
+);
 
 structure DatatypeTactics : DATATYPE_TACTICS =
 struct
@@ -185,13 +178,11 @@
 (* theory setup *)
 
 val setup =
- (DatatypesData.init #>
-  ConstructorsData.init #>
   Method.add_methods
     [("induct_tac", Method.goal_args Args.name induct_tac,
       "induct_tac emulation (dynamic instantiation!)"),
      ("case_tac", Method.goal_args Args.name exhaust_tac,
-      "datatype case_tac emulation (dynamic instantiation!)")]);
+      "datatype case_tac emulation (dynamic instantiation!)")];
 
 
 (* outer syntax *)
diff -r 5f9138bcb3d7 -r fb79144af9a3 src/ZF/Tools/typechk.ML
--- a/src/ZF/Tools/typechk.ML	Sun May 06 21:50:17 2007 +0200
+++ b/src/ZF/Tools/typechk.ML	Mon May 07 00:49:59 2007 +0200
@@ -44,7 +44,6 @@
 
 structure Data = GenericDataFun
 (
-  val name = "ZF/type-checking";
   type T = tcset
   val empty = TC {rules = [], net = Net.empty};
   val extend = I;
@@ -52,19 +51,19 @@
   fun merge _ (TC {rules, net}, TC {rules = rules', net = net'}) =
     TC {rules = Drule.merge_rules (rules, rules'),
         net = Net.merge Thm.eq_thm_prop (net, net')};
-
-  fun print context (TC {rules, ...}) =
-    Pretty.writeln (Pretty.big_list "type-checking rules:"
-      (map (ProofContext.pretty_thm (Context.proof_of context)) rules));
 );
 
-val print_tcset = Data.print o Context.Proof;
-
 val TC_add = Thm.declaration_attribute (Data.map o add_rule);
 val TC_del = Thm.declaration_attribute (Data.map o del_rule);
 
 val tcset_of = Data.get o Context.Proof;
 
+fun print_tcset ctxt =
+  let val TC {rules, ...} = tcset_of ctxt in
+    Pretty.writeln (Pretty.big_list "type-checking rules:"
+      (map (ProofContext.pretty_thm ctxt) rules))
+  end;
+
 
 (* tactics *)
 
@@ -128,7 +127,6 @@
 (* theory setup *)
 
 val setup =
-  Data.init #>
   Attrib.add_attributes [("TC", TC_att, "declaration of type-checking rule")] #>
   Method.add_methods [("typecheck", typecheck_meth, "ZF type-checking")] #>
   (fn thy => (change_simpset_of thy (fn ss => ss setSolver type_solver); thy));