# HG changeset patch
# User haftmann
# Date 1159196663 -7200
# Node ID f77bd47a70df3e61cb263453f09a8562714856e9
# Parent  da71d46b8b2ff9e257536f423c8eeb889682f5fa
changed interface in codegen_package.ML

diff -r da71d46b8b2f -r f77bd47a70df src/Pure/Tools/nbe_codegen.ML
--- a/src/Pure/Tools/nbe_codegen.ML	Mon Sep 25 17:04:22 2006 +0200
+++ b/src/Pure/Tools/nbe_codegen.ML	Mon Sep 25 17:04:23 2006 +0200
@@ -158,7 +158,7 @@
       | consts_of (A (t1, t2)) = consts_of t1 #> consts_of t2
       | consts_of (AbsN (_, t)) = consts_of t;
     val consts = consts_of t [];
-    val ctab = consts ~~ CodegenPackage.consts_of_idfs thy consts;
+    val ctab = AList.make (CodegenPackage.const_of_idf thy) consts;
     val the_const = apsnd varifyT o the o AList.lookup (op =) ctab;
     fun to_term bounds (C s) = Const (the_const s)
       | to_term bounds (V s) = Free (s, dummyT)