src/Tools/Code/code_simp.ML

   val dynamic_value: Proof.context -> term -> term
   val static_conv: { ctxt: Proof.context, simpset: simpset option, consts: string list }
     -> Proof.context -> conv
   val static_tac: { ctxt: Proof.context, simpset: simpset option, consts: string list }
     -> Proof.context -> int -> tactic
-  val setup: theory -> theory
   val trace: bool Config.T
 end;
 
 structure Code_Simp : CODE_SIMP =
 struct

   THEN' conclude_tac ctxt NONE ctxt;
 
 fun dynamic_value ctxt =
   snd o Logic.dest_equals o Thm.prop_of o dynamic_conv ctxt o Thm.cterm_of (Proof_Context.theory_of ctxt);
 
-val setup =
-  Method.setup @{binding code_simp}
+val _ = Theory.setup 
+  (Method.setup @{binding code_simp}
     (Scan.succeed (SIMPLE_METHOD' o (CHANGED_PROP oo dynamic_tac)))
-    "simplification with code equations";
+    "simplification with code equations");
 
 
 (* evaluation with static code context *)
 
 fun static_conv { ctxt, simpset, consts } =