src/HOL/Library/Old_SMT/old_smt_word.ML
changeset 58825 2065f49da190
parent 58058 1a0b18176548
--- a/src/HOL/Library/Old_SMT/old_smt_word.ML	Wed Oct 29 15:28:27 2014 +0100
+++ b/src/HOL/Library/Old_SMT/old_smt_word.ML	Wed Oct 29 17:01:44 2014 +0100
@@ -4,12 +4,7 @@
 SMT setup for words.
 *)
 
-signature OLD_SMT_WORD =
-sig
-  val setup: theory -> theory
-end
-
-structure Old_SMT_Word: OLD_SMT_WORD =
+structure Old_SMT_Word: sig end =
 struct
 
 open Word_Lib
@@ -143,9 +138,9 @@
 
 (* setup *)
 
-val setup = 
-  Context.theory_map (
-    Old_SMTLIB_Interface.add_logic (20, smtlib_logic) #>
-    setup_builtins)
+val _ = 
+  Theory.setup
+    (Context.theory_map
+      (Old_SMTLIB_Interface.add_logic (20, smtlib_logic) #> setup_builtins))
 
 end