src/Pure/pure_thy.ML

     val thms' = flat thmss';
     val thms'' =
       (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 *)
 
 fun store_thm th_atts thy =