diff -r b416573f1807 -r 3dd426ae6bea src/Pure/Isar/code.ML
--- a/src/Pure/Isar/code.ML	Wed Oct 19 22:54:26 2011 +0200
+++ b/src/Pure/Isar/code.ML	Wed Oct 19 23:07:48 2011 +0200
@@ -76,9 +76,6 @@
   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 =
@@ -1264,26 +1261,6 @@
   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
@@ -1294,8 +1271,6 @@
       || 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