Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/Pure/Tools/nbe_codegen.ML
changeset 21883 341cefa2e4da
parent 20856 9f7f0bf89e7d
child 22554 d1499fff65d8 
--- a/src/Pure/Tools/nbe_codegen.ML	Mon Dec 18 08:21:39 2006 +0100
+++ b/src/Pure/Tools/nbe_codegen.ML	Mon Dec 18 08:21:40 2006 +0100
@@ -150,7 +150,7 @@
   let
     fun to_term bounds (C s) tcount =
           let
-            val (c, ty) = CodegenPackage.const_of_idf thy s;
+            val (c, ty) = (CodegenConsts.typ_of_inst thy o the o CodegenNames.const_rev thy) s;
             val ty' = map_type_tvar (fn ((s,i),S) => TypeInfer.param (tcount + i) (s,S)) ty;
             val tcount' = tcount + maxidx_of_typ ty + 1;
           in (Const (c, ty'), tcount') end
isabelle