# HG changeset patch
# User haftmann
# Date 1256223024 -7200
# Node ID f654dafa021e110dfeed0967009034f69ddf740b
# Parent  1cefea81ec4f79b667b6993435d63f62187c1e45
close thm derivations explicitly

diff -r 1cefea81ec4f -r f654dafa021e src/Pure/Isar/code.ML
--- a/src/Pure/Isar/code.ML	Thu Oct 22 14:43:59 2009 +0200
+++ b/src/Pure/Isar/code.ML	Thu Oct 22 16:50:24 2009 +0200
@@ -670,9 +670,11 @@
 
 (* code equations *)
 
-fun gen_add_eqn default (eqn as (thm, _)) thy =
-  let val c = const_eqn thy thm
-  in change_eqns false c (add_thm thy default eqn) thy end;
+fun gen_add_eqn default (thm, proper) thy =
+  let
+    val thm' = Thm.close_derivation thm;
+    val c = const_eqn thy thm';
+  in change_eqns false c (add_thm thy default (thm', proper)) thy end;
 
 fun add_eqn thm thy =
   gen_add_eqn false (mk_eqn thy (thm, true)) thy;