# HG changeset patch
# User haftmann
# Date 1177587197 -7200
# Node ID 715d01b34abbbdee4683dd5cfc5158091df0997f
# Parent  45ac82e7b8875a0dd0a3ed191fcad95866f2c7da
clarified naming policy

diff -r 45ac82e7b887 -r 715d01b34abb src/Pure/Tools/codegen_names.ML
--- a/src/Pure/Tools/codegen_names.ML	Thu Apr 26 13:33:16 2007 +0200
+++ b/src/Pure/Tools/codegen_names.ML	Thu Apr 26 13:33:17 2007 +0200
@@ -217,13 +217,13 @@
   NameSpace.base class ^ "_" ^ NameSpace.base tyco) thyname_of_instance;
 
 fun force_thyname thy (const as (c, opt_tyco)) =
-  case AxClass.class_of_param thy c
-   of SOME class => (case opt_tyco
-       of SOME tyco => SOME (thyname_of_instance thy (class, tyco))
-        | NONE => SOME (thyname_of_class thy class))
-    | NONE => (case CodegenData.get_datatype_of_constr thy const
+  case CodegenData.get_datatype_of_constr thy const
    of SOME dtco => SOME (thyname_of_tyco thy dtco)
-    | NONE => NONE);
+    | NONE => (case AxClass.class_of_param thy c
+       of SOME class => (case opt_tyco
+           of SOME tyco => SOME (thyname_of_instance thy (class, tyco))
+            | NONE => SOME (thyname_of_class thy class))
+        | NONE => NONE);
 
 fun const_policy thy (const as (c, opt_tyco)) =
   case force_thyname thy const