src/Pure/codegen.ML
changeset 16364 dc9f7066d80a
parent 16331 386ce655d694
child 16458 4c6fd0c01d28
--- a/src/Pure/codegen.ML	Sat Jun 11 22:15:47 2005 +0200
+++ b/src/Pure/codegen.ML	Sat Jun 11 22:15:48 2005 +0200
@@ -300,7 +300,7 @@
   let
     val {codegens, tycodegens, consts, types, attrs, preprocs, test_params} =
       CodegenData.get thy;
-    val tc = Sign.intern_tycon (sign_of thy) s
+    val tc = Sign.intern_type (sign_of thy) s
   in
     (case assoc (types, tc) of
        NONE => CodegenData.put {codegens = codegens,
@@ -342,11 +342,11 @@
   end;
 
 fun mk_const_id sg s =
-  let val s' = mk_id (Sign.extern sg Sign.constK s)
+  let val s' = mk_id (Sign.extern_const sg s)
   in if s' mem ThmDatabase.ml_reserved then s' ^ "_const" else s' end;
 
 fun mk_type_id sg s =
-  let val s' = mk_id (Sign.extern sg Sign.typeK s)
+  let val s' = mk_id (Sign.extern_type sg s)
   in if s' mem ThmDatabase.ml_reserved then s' ^ "_type" else s' end;
 
 fun rename_terms ts =