diff -r 9f60d493c8fe -r 9f7f0bf89e7d src/Pure/Tools/nbe_codegen.ML
--- a/src/Pure/Tools/nbe_codegen.ML	Wed Oct 04 14:17:46 2006 +0200
+++ b/src/Pure/Tools/nbe_codegen.ML	Wed Oct 04 14:17:47 2006 +0200
@@ -1,4 +1,5 @@
-(*  ID:         $Id$
+(*  Title:      Pure/nbe_codegen.ML
+    ID:         $Id$
     Author:     Klaus Aehlig, LMU Muenchen; Tobias Nipkow, TU Muenchen
 
 Code generator for "normalization by evaluation".
@@ -145,21 +146,25 @@
 
 open NBE_Eval;
 
-val tcount = ref 0;
-
-fun varifyT ty =
-  let 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 tcount := !tcount+1; ty' end;
-
 fun nterm_to_term thy t =
   let
-   fun to_term bounds (C s) = Const ((apsnd varifyT o CodegenPackage.const_of_idf thy) s)
-     | to_term bounds (V s) = Free (s, dummyT)
-     | to_term bounds (B i) = Bound (find_index (fn j => i = j) bounds)
-     | to_term bounds (A (t1, t2)) = to_term bounds t1 $ to_term bounds t2
-     | to_term bounds (AbsN (i, t)) =
-          Abs("u", dummyT, to_term (i::bounds) t);
-  in tcount := 0; to_term [] t end;
+    fun to_term bounds (C s) tcount =
+          let
+            val (c, ty) = CodegenPackage.const_of_idf 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
+      | to_term bounds (V s) tcount = (Free (s, dummyT), tcount)
+      | to_term bounds (B i) tcount = (Bound (find_index (fn j => i = j) bounds), tcount)
+      | to_term bounds (A (t1, t2)) tcount =
+          tcount
+          |> to_term bounds t1
+          ||>> to_term bounds t2
+          |-> (fn (t1', t2') => pair (t1' $ t2'))
+      | to_term bounds (AbsN (i, t)) tcount =
+          tcount
+          |> to_term (i :: bounds) t
+          |-> (fn t' => pair (Abs ("u", dummyT, t')));
+  in fst (to_term [] t 0) end;
 
 end;