src/HOL/Tools/refute.ML

       bounds    : interpretation list,
       wellformed: prop_formula
     };
 
 
-  structure RefuteDataArgs =
-  struct
-    val name = "HOL/refute";
+  structure RefuteData = TheoryDataFun
+  (
     type T =
       {interpreters: (string * (theory -> model -> arguments -> Term.term ->
         (interpretation * model * arguments) option)) list,
        printers: (string * (theory -> model -> Term.term -> interpretation ->
         (int -> bool) -> Term.term option)) list,

       ({interpreters = in1, printers = pr1, parameters = pa1},
        {interpreters = in2, printers = pr2, parameters = pa2}) =
       {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);
+  );
 
 
 (* ------------------------------------------------------------------------- *)
 (* interpret: interprets the term 't' using a suitable interpreter; returns  *)
 (*            the interpretation and a (possibly extended) model that keeps  *)

 (* ------------------------------------------------------------------------- *)
 
   (* (theory -> theory) list *)
 
   val setup =
-     RefuteData.init #>
      add_interpreter "stlc"    stlc_interpreter #>
      add_interpreter "Pure"    Pure_interpreter #>
      add_interpreter "HOLogic" HOLogic_interpreter #>
      add_interpreter "set"     set_interpreter #>
      add_interpreter "IDT"             IDT_interpreter #>