corrected slip: must keep constant map, not type map; tuned code
authorhaftmann
Mon, 08 Nov 2010 10:56:48 +0100
changeset 40422 d425d1ed82af
parent 40421 b41aabb629ce
child 40423 6923b39ad91f
corrected slip: must keep constant map, not type map; tuned code
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;