src/Tools/Code/code_ml.ML

 
 signature CODE_ML =
 sig
   val target_SML: string
   val target_OCaml: string
-  val setup: theory -> theory
 end;
 
 structure Code_ML : CODE_ML =
 struct
 

     print_typ (INFX (1, X)) ty1,
     str "->",
     print_typ (INFX (1, R)) ty2
   );
 
-val setup =
-  Code_Target.add_language
+val _ = Theory.setup
+  (Code_Target.add_language
     (target_SML, { serializer = serializer_sml, literals = literals_sml,
       check = { env_var = "ISABELLE_PROCESS",
         make_destination = fn p => Path.append p (Path.explode "ROOT.ML"),
         make_command = fn _ =>
           "\"$ISABELLE_PROCESS\" -r -q -e 'datatype ref = datatype Unsynchronized.ref; use \"ROOT.ML\" handle _ => exit 1' Pure" } })

       "in", "include", "inherit", "initializer", "lazy", "let", "match", "method",
       "module", "mutable", "new", "object", "of", "open", "or", "private", "rec",
       "sig", "struct", "then", "to", "true", "try", "type", "val",
       "virtual", "when", "while", "with"
     ]
-  #> fold (Code_Target.add_reserved target_OCaml) ["failwith", "mod", "Big_int"];
+  #> fold (Code_Target.add_reserved target_OCaml) ["failwith", "mod", "Big_int"]);
 
 end; (*struct*)