close code theorems explicitly after preprocessing

--- a/src/Pure/Isar/code.ML	Mon Oct 22 17:09:49 2012 +0200
+++ b/src/Pure/Isar/code.ML	Mon Oct 22 19:02:36 2012 +0200
@@ -31,6 +31,7 @@
   val empty_cert: theory -> string -> cert
   val cert_of_eqns: theory -> string -> (thm * bool) list -> cert
   val constrain_cert: theory -> sort list -> cert -> cert
+  val conclude_cert: cert -> cert
   val typargs_deps_of_cert: theory -> cert -> (string * sort) list * (string * typ list) list
   val equations_of_cert: theory -> cert -> ((string * sort) list * typ)
     * (((term * string option) list * (term * string option)) * (thm option * bool)) list
@@ -782,6 +783,13 @@
   | constrain_cert thy sorts (Abstract (abs_thm, tyco)) =
       Abstract (snd (constrain_thm thy (fst (typscheme_abs thy abs_thm)) sorts abs_thm), tyco);
 
+fun conclude_cert (Equations (cert_thm, propers)) =
+      (Equations (Thm.close_derivation cert_thm, propers))
+  | conclude_cert (cert as Projection _) =
+      cert
+  | conclude_cert (Abstract (abs_thm, tyco)) =
+      (Abstract (Thm.close_derivation abs_thm, tyco));
+
 fun typscheme_of_cert thy (Equations (cert_thm, _)) =
       fst (get_head thy cert_thm)
   | typscheme_of_cert thy (Projection (proj, _)) =

--- a/src/Tools/Code/code_preproc.ML	Mon Oct 22 17:09:49 2012 +0200
+++ b/src/Tools/Code/code_preproc.ML	Mon Oct 22 19:02:36 2012 +0200
@@ -395,7 +395,9 @@
   else let
     val lhs = map_index (fn (k, (v, _)) =>
       (v, snd (Vargraph.get_node vardeps (Fun c, k)))) proto_lhs;
-    val cert = Code.constrain_cert thy (map (Sign.minimize_sort thy o snd) lhs) proto_cert;
+    val cert = proto_cert
+      |> Code.constrain_cert thy (map (Sign.minimize_sort thy o snd) lhs)
+      |> Code.conclude_cert;
     val (vs, rhss') = Code.typargs_deps_of_cert thy cert;
     val eqngr' = Graph.new_node (c, (vs, cert)) eqngr;
   in (map (pair c) rhss' @ rhss, eqngr') end;