diff -r 796ae7fa1049 -r 8ef25fe585a8 src/Pure/codegen.ML
--- a/src/Pure/codegen.ML	Fri Sep 15 22:56:08 2006 +0200
+++ b/src/Pure/codegen.ML	Fri Sep 15 22:56:13 2006 +0200
@@ -1010,7 +1010,7 @@
       | strip t = t;
     val (gi, frees) = Logic.goal_params
       (prop_of (snd (snd (Proof.get_goal (Toplevel.proof_of st))))) i;
-    val gi' = ObjectLogic.atomize_term thy (map_term_types
+    val gi' = ObjectLogic.atomize_term thy (map_types
       (map_type_tfree (fn p as (s, _) =>
         the_default (the_default (TFree p) default_type)
           (AList.lookup (op =) tvinsts s))) (subst_bounds (frees, strip gi)));