# HG changeset patch
# User wenzelm
# Date 928518716 -7200
# Node ID 4b1bd69dfe0b4bd8c695c3c16bd695f528323e91
# Parent  26d64339c25a3e75110ae7fad3957052a5401a77
fixed BUG in have_thmss: return thy';

diff -r 26d64339c25a -r 4b1bd69dfe0b src/Pure/pure_thy.ML
--- a/src/Pure/pure_thy.ML	Fri Jun 04 19:51:26 1999 +0200
+++ b/src/Pure/pure_thy.ML	Fri Jun 04 19:51:56 1999 +0200
@@ -275,7 +275,7 @@
       (case opt_bname of
         None => thms'
       | Some bname => enter_thmx (Theory.sign_of thy') name_multi (bname, thms'));
-  in (thy, thms'') end;
+  in (thy', thms'') end;
 
 
 (* store_thm *)