diff -r b41aabb629ce -r d425d1ed82af src/Tools/Code/code_runtime.ML
--- a/src/Tools/Code/code_runtime.ML	Mon Nov 08 10:43:24 2010 +0100
+++ b/src/Tools/Code/code_runtime.ML	Mon Nov 08 10:56:48 2010 +0100
@@ -226,7 +226,7 @@
     val consts' = fold (insert (op =)) new_consts consts;
     val acc_code = Lazy.lazy (fn () =>
       evaluation_code (ProofContext.theory_of ctxt) "Code" tycos' consts'
-      |> apsnd fst);
+      |> apsnd snd);
   in Code_Antiq_Data.put ((tycos', consts'), (false, acc_code)) ctxt end;
 
 fun register_const const = register_code [] [const];
@@ -238,8 +238,7 @@
   let
     val (_, (_, acc_code)) = Code_Antiq_Data.get ctxt;
     val (ml_code, consts_map) = Lazy.force acc_code;
-    val ml_code = if is_first then ml_code
-      else "";
+    val ml_code = if is_first then ml_code else "";
     val all_struct_name = "Isabelle";
   in (ml_code, print_const const all_struct_name consts_map) end;