# HG changeset patch
# User haftmann
# Date 1256273630 -7200
# Node ID c6693f51e4e4fbec1435d6cdab65895ea61cf036
# Parent  e6eda76ad49e4d84cb990d5d08848c65221e4b3b# Parent  f654dafa021e110dfeed0967009034f69ddf740b
merged

diff -r e6eda76ad49e -r c6693f51e4e4 src/Pure/Isar/code.ML
--- a/src/Pure/Isar/code.ML	Fri Oct 23 09:20:22 2009 +1100
+++ b/src/Pure/Isar/code.ML	Fri Oct 23 06:53:50 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;