# HG changeset patch
# User blanchet
# Date 1348646460 -7200
# Node ID e8c57e59cbf810dea299732553dc3d547b89371f
# Parent  55e798614c452e25966319d3bec63930fd2846f5
got rid of other instance of shaky "Thm.generalize"

diff -r 55e798614c45 -r e8c57e59cbf8 src/HOL/BNF/Tools/bnf_def.ML
--- a/src/HOL/BNF/Tools/bnf_def.ML	Wed Sep 26 10:01:00 2012 +0200
+++ b/src/HOL/BNF/Tools/bnf_def.ML	Wed Sep 26 10:01:00 2012 +0200
@@ -688,9 +688,10 @@
     val bnf_bd_As = mk_bnf_t As' bnf_bd;
     val bnf_wit_As = map (apsnd (mk_bnf_t As')) bnf_wits;
 
+    val pre_names_lthy = lthy;
     val (((((((((((((((((((((((((fs, fs_copy), gs), hs), p), (x, x')), (y, y')), (z, z')), zs), As),
       As_copy), Xs), B1s), B2s), f1s), f2s), e1s), e2s), p1s), p2s), bs), (Rs, Rs')), Rs_copy), Ss),
-      (Qs, Qs')), _) = lthy
+      (Qs, Qs')), names_lthy) = pre_names_lthy
       |> mk_Frees "f" (map2 (curry (op -->)) As' Bs')
       ||>> mk_Frees "f" (map2 (curry (op -->)) As' Bs')
       ||>> mk_Frees "g" (map2 (curry (op -->)) Bs' Cs)
@@ -1137,8 +1138,7 @@
           in
             unfold_thms lthy (bnf_srel_def :: @{thm converse_iff} :: mem_Collect_etc)
               (srel_converse_thm' RS eqset_imp_iff_pair)
-            |> Drule.zero_var_indexes
-            |> Thm.generalize (map (fst o dest_TFree) (As' @ Bs'), map fst Qs') 1
+            |> singleton (Proof_Context.export names_lthy pre_names_lthy)
           end;
 
         val rel_flip = Lazy.lazy mk_rel_flip;
diff -r 55e798614c45 -r e8c57e59cbf8 src/HOL/BNF/Tools/bnf_fp_sugar.ML
--- a/src/HOL/BNF/Tools/bnf_fp_sugar.ML	Wed Sep 26 10:01:00 2012 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_sugar.ML	Wed Sep 26 10:01:00 2012 +0200
@@ -801,8 +801,7 @@
               Skip_Proof.prove lthy [] [] goal (tac o #context)
               |> Thm.close_derivation;
           in
-            (map2 (map2 prove) fold_goalss fold_tacss,
-             map2 (map2 prove) rec_goalss rec_tacss)
+            (map2 (map2 prove) fold_goalss fold_tacss, map2 (map2 prove) rec_goalss rec_tacss)
           end;
 
         val simp_thmss = mk_simp_thmss wrap_ress rec_thmss fold_thmss;