# HG changeset patch
# User haftmann
# Date 1283272716 -7200
# Node ID 2cf3d8305b47eb198d71224b0a79d1ef9748d02f
# Parent  94d239bbb61851559e3e70f9ab87793254c2ab94
corrected misbehaved additional qualification of generated names

diff -r 94d239bbb618 -r 2cf3d8305b47 src/Tools/Code/code_eval.ML
--- a/src/Tools/Code/code_eval.ML	Tue Aug 31 17:46:27 2010 +0200
+++ b/src/Tools/Code/code_eval.ML	Tue Aug 31 18:38:36 2010 +0200
@@ -151,17 +151,13 @@
   const (SOME (Code_Printer.simple_const_syntax (0, (K o K o K) const')));
 
 fun process (code_body, (tyco_map, (constr_map, const_map))) module_name NONE thy =
-      let
-        val pr = Code_Printer.str o Long_Name.append module_name;
-      in
-        thy
-        |> Code_Target.add_reserved target module_name
-        |> Context.theory_map
-          (ML_Context.exec (fn () => ML_Context.eval_text true Position.none code_body))
-        |> fold (add_eval_tyco o apsnd pr) tyco_map
-        |> fold (add_eval_constr o apsnd pr) constr_map
-        |> fold (add_eval_const o apsnd pr) const_map
-      end
+      thy
+      |> Code_Target.add_reserved target module_name
+      |> Context.theory_map
+        (ML_Context.exec (fn () => ML_Context.eval_text true Position.none code_body))
+      |> fold (add_eval_tyco o apsnd Code_Printer.str) tyco_map
+      |> fold (add_eval_constr o apsnd Code_Printer.str) constr_map
+      |> fold (add_eval_const o apsnd Code_Printer.str) const_map
   | process (code_body, _) _ (SOME file_name) thy =
       let
         val preamble =