# HG changeset patch
# User haftmann
# Date 1164187222 -3600
# Node ID 51239d45247bc143d6f9f0b2cd87004b52ebe397
# Parent  cda5cd8bfd1644c2c4fd0050764b16e1ab4ca992
forced name prefix for class operations

diff -r cda5cd8bfd16 -r 51239d45247b src/Pure/Tools/codegen_names.ML
--- a/src/Pure/Tools/codegen_names.ML	Wed Nov 22 10:20:20 2006 +0100
+++ b/src/Pure/Tools/codegen_names.ML	Wed Nov 22 10:20:22 2006 +0100
@@ -2,7 +2,7 @@
     ID:         $Id$
     Author:     Florian Haftmann, TU Muenchen
 
-Name policies for code generation: prefixing any name by corresponding theory name,
+Naming policies for code generation: prefixing any name by corresponding theory name,
 conversion to alphanumeric representation, shallow name spaces.
 Mappings are incrementally cached.
 *)
@@ -219,7 +219,6 @@
       ^ "perhaps try " ^ quote (NameSpace.pack mns'))
   end
 
-
 fun purify_var "" = "x"
   | purify_var v =
       if nth (explode v) 0 = "'"
@@ -244,14 +243,16 @@
 fun instance_policy thy = policy thy (fn (class, tyco) => 
   NameSpace.base class ^ "_" ^ NameSpace.base tyco) thyname_of_instance;
 
-fun force_thyname thy (c, tys) =
+fun force_thyname thy (const as (c, tys)) =
   case AxClass.class_of_param thy c
    of SOME class => (case tys
        of [Type (tyco, _)] => SOME (thyname_of_instance thy (class, tyco))
-        | _ => NONE)
-    | NONE => (case CodegenConsts.find_def thy (c, tys)
+        | _ => SOME (thyname_of_class thy class))
+    | NONE => (case CodegenData.get_datatype_of_constr thy const
+   of SOME dtco => SOME (thyname_of_tyco thy dtco)
+    | NONE => (case CodegenConsts.find_def thy const
    of SOME ((thyname, _), _) => SOME thyname
-    | NONE => NONE);
+    | NONE => NONE));
 
 fun const_policy thy (c, tys) =
   case force_thyname thy (c, tys)