diff -r d480d1d7c544 -r 2065f49da190 src/HOL/Library/refute.ML
--- a/src/HOL/Library/refute.ML	Wed Oct 29 15:28:27 2014 +0100
+++ b/src/HOL/Library/refute.ML	Wed Oct 29 17:01:44 2014 +0100
@@ -52,8 +52,6 @@
   val refute_goal :
     Proof.context -> (string * string) list -> thm -> int -> string
 
-  val setup : theory -> theory
-
 (* ------------------------------------------------------------------------- *)
 (* Additional functions used by Nitpick (to be factored out)                 *)
 (* ------------------------------------------------------------------------- *)
@@ -2926,37 +2924,33 @@
 
 
 (* ------------------------------------------------------------------------- *)
-(* use 'setup Refute.setup' in an Isabelle theory to initialize the 'Refute' *)
-(* structure                                                                 *)
-(* ------------------------------------------------------------------------- *)
-
-(* ------------------------------------------------------------------------- *)
 (* Note: the interpreters and printers are used in reverse order; however,   *)
 (*       an interpreter that can handle non-atomic terms ends up being       *)
 (*       applied before the 'stlc_interpreter' breaks the term apart into    *)
 (*       subterms that are then passed to other interpreters!                *)
 (* ------------------------------------------------------------------------- *)
 (* FIXME formal @{const_name} for some entries (!??) *)
-val setup =
-   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 #>
-   add_interpreter "IDT_constructor" IDT_constructor_interpreter #>
-   add_interpreter "IDT_recursion"   IDT_recursion_interpreter #>
-   add_interpreter "Finite_Set.card"    Finite_Set_card_interpreter #>
-   add_interpreter "Finite_Set.finite"  Finite_Set_finite_interpreter #>
-   add_interpreter "Nat_Orderings.less" Nat_less_interpreter #>
-   add_interpreter "Nat_HOL.plus"       Nat_plus_interpreter #>
-   add_interpreter "Nat_HOL.minus"      Nat_minus_interpreter #>
-   add_interpreter "Nat_HOL.times"      Nat_times_interpreter #>
-   add_interpreter "List.append" List_append_interpreter #>
-   add_interpreter "Product_Type.prod.fst" Product_Type_fst_interpreter #>
-   add_interpreter "Product_Type.prod.snd" Product_Type_snd_interpreter #>
-   add_printer "stlc" stlc_printer #>
-   add_printer "set" set_printer #>
-   add_printer "IDT"  IDT_printer;
+val _ =
+  Theory.setup
+   (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 #>
+    add_interpreter "IDT_constructor" IDT_constructor_interpreter #>
+    add_interpreter "IDT_recursion"   IDT_recursion_interpreter #>
+    add_interpreter "Finite_Set.card"    Finite_Set_card_interpreter #>
+    add_interpreter "Finite_Set.finite"  Finite_Set_finite_interpreter #>
+    add_interpreter "Nat_Orderings.less" Nat_less_interpreter #>
+    add_interpreter "Nat_HOL.plus"       Nat_plus_interpreter #>
+    add_interpreter "Nat_HOL.minus"      Nat_minus_interpreter #>
+    add_interpreter "Nat_HOL.times"      Nat_times_interpreter #>
+    add_interpreter "List.append" List_append_interpreter #>
+    add_interpreter "Product_Type.prod.fst" Product_Type_fst_interpreter #>
+    add_interpreter "Product_Type.prod.snd" Product_Type_snd_interpreter #>
+    add_printer "stlc" stlc_printer #>
+    add_printer "set" set_printer #>
+    add_printer "IDT"  IDT_printer);