--- a/Nominal/Nominal2.thy	Tue Dec 21 10:28:08 2010 +0000
+++ b/Nominal/Nominal2.thy	Wed Dec 22 09:13:25 2010 +0000
@@ -307,6 +307,7 @@
             RANGE (map2 (case_tac context c bn_finite_thms eq_iff_thms bn_eqvt permute_bns perm_bn_alphas) 
                       (prems' ~~ bclausesss) exhausts')]
         end)
+    |> ProofContext.export lthy'' lthy
   end
 *}
 
@@ -847,6 +848,7 @@
      ||>> Local_Theory.note ((thms_suffix "induct", []), [qinduct]) 
      ||>> Local_Theory.note ((thms_suffix "inducts", []), qinducts)
      ||>> Local_Theory.note ((thms_suffix "exhaust", []), qexhausts)
+     ||>> Local_Theory.note ((thms_suffix "strong_exhaust", []), qstrong_exhaust_thms)
      ||>> Local_Theory.note ((thms_suffix "supports", []), qsupports_thms)
      ||>> Local_Theory.note ((thms_suffix "fsupp", []), qfsupp_thms)
      ||>> Local_Theory.note ((thms_suffix "supp", []), qsupp_constrs)