clarified naming policy
authorhaftmann
Thu, 26 Apr 2007 13:33:17 +0200
changeset 22807 715d01b34abb
parent 22806 45ac82e7b887
child 22808 a7daa74e2980
clarified naming policy
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