export right sorts

--- a/src/HOL/Tools/BNF/bnf_lfp_compat.ML	Mon Sep 08 15:12:35 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_compat.ML	Mon Sep 08 15:54:33 2014 +0200
@@ -217,7 +217,8 @@
         SOME (fp_sugar as {fp = Least_FP, ...}) => fp_sugar
       | _ => not_datatype s);
 
-    val fpTs0 as Type (_, var_As) :: _ = #Ts (#fp_res (lfp_sugar_of (hd fpT_names0)));
+    val fpTs0 as Type (_, var_As) :: _ =
+      map (#T o lfp_sugar_of o fst o dest_Type) (#Ts (#fp_res (lfp_sugar_of (hd fpT_names0))));
     val fpT_names = map (fst o dest_Type) fpTs0;
 
     val _ = check_names (op =) (fpT_names0, fpT_names) orelse not_mutually_recursive fpT_names0;

--- a/src/HOL/Tools/Quickcheck/random_generators.ML	Mon Sep 08 15:12:35 2014 +0200
+++ b/src/HOL/Tools/Quickcheck/random_generators.ML	Mon Sep 08 15:54:33 2014 +0200
@@ -119,7 +119,7 @@
 fun random_aux_primrec_multi auxname [eq] lthy =
       lthy
       |> random_aux_primrec eq
-      |>> (fn simp => [simp])
+      |>> single
   | random_aux_primrec_multi auxname (eqs as _ :: _ :: _) lthy =
       let
         val thy = Proof_Context.theory_of lthy;
@@ -147,14 +147,13 @@
             fun tac { context = ctxt, prems = _ } =
               ALLGOALS (simp_tac (put_simpset HOL_ss ctxt addsimps proj_simps))
               THEN ALLGOALS (EqSubst.eqsubst_tac ctxt [0] [aux_simp])
-              THEN ALLGOALS (simp_tac
-                (put_simpset HOL_ss ctxt addsimps [@{thm fst_conv}, @{thm snd_conv}]));
+              THEN ALLGOALS (simp_tac (put_simpset HOL_ss ctxt addsimps @{thms fst_conv snd_conv}));
           in (map (fn prop => Goal.prove_sorry lthy [v] [] prop tac) eqs, lthy) end;
       in
         lthy
         |> random_aux_primrec aux_eq'
         ||>> fold_map Local_Theory.define proj_defs
-        |-> (fn (aux_simp, proj_defs) => prove_eqs aux_simp proj_defs)
+        |-> uncurry prove_eqs
       end;
 
 fun random_aux_specification prfx name eqs lthy =
@@ -176,7 +175,7 @@
   in
     lthy
     |> random_aux_primrec_multi (name ^ prfx) proto_eqs
-    |-> (fn proto_simps => prove_simps proto_simps)
+    |-> prove_simps
     |-> (fn simps => Local_Theory.note
       ((b, Code.add_default_eqn_attrib :: @{attributes [simp, nitpick_simp]}), simps))
     |> snd