src/Pure/Isar/code.ML

   val get_cert: theory -> ((thm * bool) list -> (thm * bool) list) -> string -> cert
   val get_case_scheme: theory -> string -> (int * (int * string list)) option
   val get_case_cong: theory -> string -> thm option
   val undefineds: theory -> string list
   val print_codesetup: theory -> unit
-
-  (*infrastructure*)
-  val set_code_target_attr: (string -> thm -> theory -> theory) -> theory -> theory
 end;
 
 signature CODE_DATA_ARGS =
 sig
   type T

         (map_types Logic.varifyT_global (mk_proj tyco vs ty abs rep), tyco))
     |> Abstype_Interpretation.data (tyco, serial ())
   end;
 
 
-(** infrastructure **)
-
-(* cf. src/HOL/Tools/recfun_codegen.ML *)
-
-structure Code_Target_Attr = Theory_Data
-(
-  type T = (string -> thm -> theory -> theory) option;
-  val empty = NONE;
-  val extend = I;
-  val merge = merge_options;
-);
-
-fun set_code_target_attr f = Code_Target_Attr.map (K (SOME f));
-
-fun code_target_attr prefix thm thy =
-  let
-    val attr = the_default ((K o K) I) (Code_Target_Attr.get thy);
-  in thy |> add_warning_eqn thm |> attr prefix thm end;
-
-
 (* setup *)
 
 val _ = Context.>> (Context.map_theory
   (let
     fun mk_attribute f = Thm.declaration_attribute (fn thm => Context.mapping (f thm) I);
     val code_attribute_parser =
       Args.del |-- Scan.succeed (mk_attribute del_eqn)
       || Args.$$$ "nbe" |-- Scan.succeed (mk_attribute add_nbe_eqn)
       || Args.$$$ "abstype" |-- Scan.succeed (mk_attribute add_abstype)
       || Args.$$$ "abstract" |-- Scan.succeed (mk_attribute add_abs_eqn)
-      || (Args.$$$ "target" |-- Args.colon |-- Args.name >>
-           (mk_attribute o code_target_attr))
       || Scan.succeed (mk_attribute add_warning_eqn);
   in
     Datatype_Interpretation.init
     #> Attrib.setup (Binding.name "code") (Scan.lift code_attribute_parser)
         "declare theorems for code generation"