diff -r a84351e7490d -r 1ec0a3ff229e src/Tools/Code/code_eval.ML
--- a/src/Tools/Code/code_eval.ML	Sat Feb 06 23:26:17 2010 +0100
+++ b/src/Tools/Code/code_eval.ML	Sun Feb 07 18:04:48 2010 +0100
@@ -107,25 +107,25 @@
     val _ = map2 check_base constrs constrs'';
   in "datatype " ^ tyco'' ^ " = datatype " ^ Long_Name.append all_struct_name tyco'' end;
 
-fun print_code struct_name is_first print_it ctxt =
+fun print_code is_first print_it ctxt =
   let
     val (_, (_, (struct_code_name, acc_code))) = CodeAntiqData.get ctxt;
     val (ml_code, (tycos_map, consts_map)) = Lazy.force acc_code;
     val ml_code = if is_first then ml_code
       else "";
-    val all_struct_name = Long_Name.append struct_name struct_code_name;
+    val all_struct_name = "Isabelle." ^ struct_code_name;
   in (ml_code, print_it all_struct_name tycos_map consts_map) end;
 
 in
 
-fun ml_code_antiq raw_const {struct_name, background} =
+fun ml_code_antiq raw_const background =
   let
     val const = Code.check_const (ProofContext.theory_of background) raw_const;
     val is_first = is_first_occ background;
     val background' = register_const const background;
-  in (print_code struct_name is_first (print_const const), background') end;
+  in (print_code is_first (print_const const), background') end;
 
-fun ml_code_datatype_antiq (raw_tyco, raw_constrs) {struct_name, background} =
+fun ml_code_datatype_antiq (raw_tyco, raw_constrs) background =
   let
     val thy = ProofContext.theory_of background;
     val tyco = Sign.intern_type thy raw_tyco;
@@ -135,7 +135,7 @@
       else error ("Type " ^ quote tyco ^ ": given constructors diverge from real constructors")
     val is_first = is_first_occ background;
     val background' = register_datatype tyco constrs background;
-  in (print_code struct_name is_first (print_datatype tyco constrs), background') end;
+  in (print_code is_first (print_datatype tyco constrs), background') end;
 
 end; (*local*)