src/HOL/Tools/Function/fun.ML

     (Attrib.binding * term) list -> Function_Common.function_config ->
     local_theory -> Proof.context
   val add_fun_cmd : (binding * string option * mixfix) list ->
     (Attrib.binding * string) list -> Function_Common.function_config ->
     bool -> local_theory -> Proof.context
-
-  val setup : theory -> theory
 end
 
 structure Function_Fun : FUNCTION_FUN =
 struct
 

       (flat spliteqs, restore_spec, sort, case_names)
     end
   else
     Function_Common.empty_preproc check_defs config ctxt fixes spec
 
-val setup =
-  Context.theory_map (Function_Common.set_preproc sequential_preproc)
+val _ = Theory.setup (Context.theory_map (Function_Common.set_preproc sequential_preproc))
+
 
 
 val fun_config = FunctionConfig { sequential=true, default=NONE,
   domintros=false, partials=false }