src/Pure/Tools/codegen_package.ML
changeset 22423 c1836b14c63a
parent 22396 6c7f9207fa9e
child 22464 164e7be27736
--- a/src/Pure/Tools/codegen_package.ML	Fri Mar 09 08:45:50 2007 +0100
+++ b/src/Pure/Tools/codegen_package.ML	Fri Mar 09 08:45:53 2007 +0100
@@ -148,11 +148,7 @@
       let
         fun defgen_datatype trns =
           let
-            val (vs, cos) = case CodegenData.get_datatype thy tyco
-             of SOME x => x
-              | NONE => (Name.invents Name.context "'a" (Sign.arity_number thy tyco)
-                  |> map (rpair (Sign.defaultS thy)) , [])
-              (*FIXME move to CodegenData*)
+            val (vs, cos) = CodegenData.get_datatype thy tyco;
           in
             trns
             |> fold_map (exprgen_tyvar_sort thy algbr funcgr strct) vs