--- 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;