src/HOL/Codatatype/Tools/bnf_comp.ML

             mk_comp_set_bd_tac context comp_set_alt single_set_bds)
           comp_set_alt_thms single_set_bd_thmss
         end;
 
     val comp_in_alt_thm =
-      if ! quick_and_dirty then
-        no_thm
-      else
-        let
-          val comp_in = mk_in Asets comp_sets CCA;
-          val comp_in_alt = mk_in (map2 (mk_in Asets) inner_setss CAs) outer_sets CCA;
-          val goal = fold_rev Logic.all Asets (mk_Trueprop_eq (comp_in, comp_in_alt));
-        in
-          Skip_Proof.prove lthy [] [] goal
-            (fn {context, ...} => mk_comp_in_alt_tac context comp_set_alt_thms)
-          |> Thm.close_derivation
-        end;
+      let
+        val comp_in = mk_in Asets comp_sets CCA;
+        val comp_in_alt = mk_in (map2 (mk_in Asets) inner_setss CAs) outer_sets CCA;
+        val goal = fold_rev Logic.all Asets (mk_Trueprop_eq (comp_in, comp_in_alt));
+      in
+        Skip_Proof.prove lthy [] [] goal
+          (fn {context, ...} => mk_comp_in_alt_tac context comp_set_alt_thms)
+        |> Thm.close_derivation
+      end;
 
     fun comp_in_bd_tac _ =
       mk_comp_in_bd_tac comp_in_alt_thm (map in_bd_of_bnf inners) (in_bd_of_bnf outer)
         (map bd_Cinfinite_of_bnf inners) (bd_Card_order_of_bnf outer);
 

     val killN_set_bd_tacs =
       map (fn thm => fn _ => mk_killN_set_bd_tac (bd_Card_order_of_bnf bnf) thm)
         (drop n (set_bd_of_bnf bnf));
 
     val killN_in_alt_thm =
-      if ! quick_and_dirty then
-        no_thm
-      else
-        let
-          val killN_in = mk_in Asets killN_sets T;
-          val killN_in_alt = mk_in (map HOLogic.mk_UNIV killedAs @ Asets) bnf_sets T;
-          val goal = fold_rev Logic.all Asets (mk_Trueprop_eq (killN_in, killN_in_alt));
-        in
-          Skip_Proof.prove lthy [] [] goal (K killN_in_alt_tac) |> Thm.close_derivation
-        end;
+      let
+        val killN_in = mk_in Asets killN_sets T;
+        val killN_in_alt = mk_in (map HOLogic.mk_UNIV killedAs @ Asets) bnf_sets T;
+        val goal = fold_rev Logic.all Asets (mk_Trueprop_eq (killN_in, killN_in_alt));
+      in
+        Skip_Proof.prove lthy [] [] goal (K killN_in_alt_tac) |> Thm.close_derivation
+      end;
 
     fun killN_in_bd_tac _ =
       mk_killN_in_bd_tac n (live > n) killN_in_alt_thm (in_bd_of_bnf bnf)
          (bd_Card_order_of_bnf bnf) (bd_Cinfinite_of_bnf bnf) (bd_Cnotzero_of_bnf bnf);
     fun killN_map_wpull_tac _ =

       else
         replicate n (K (mk_liftN_set_bd_tac (bd_Card_order_of_bnf bnf))) @
         (map (fn thm => fn _ => rtac thm 1) (set_bd_of_bnf bnf));
 
     val liftN_in_alt_thm =
-      if ! quick_and_dirty then
-        no_thm
-      else
-        let
-          val liftN_in = mk_in Asets liftN_sets T;
-          val liftN_in_alt = mk_in (drop n Asets) bnf_sets T;
-          val goal = fold_rev Logic.all Asets (mk_Trueprop_eq (liftN_in, liftN_in_alt));
-        in
-          Skip_Proof.prove lthy [] [] goal (K liftN_in_alt_tac) |> Thm.close_derivation
-        end;
+      let
+        val liftN_in = mk_in Asets liftN_sets T;
+        val liftN_in_alt = mk_in (drop n Asets) bnf_sets T;
+        val goal = fold_rev Logic.all Asets (mk_Trueprop_eq (liftN_in, liftN_in_alt));
+      in
+        Skip_Proof.prove lthy [] [] goal (K liftN_in_alt_tac) |> Thm.close_derivation
+      end;
 
     fun liftN_in_bd_tac _ =
       mk_liftN_in_bd_tac n liftN_in_alt_thm (in_bd_of_bnf bnf) (bd_Card_order_of_bnf bnf);
     fun liftN_map_wpull_tac _ =
       mk_map_wpull_tac liftN_in_alt_thm [] (map_wpull_of_bnf bnf);

     fun permute_bd_card_order_tac _ = rtac (bd_card_order_of_bnf bnf) 1;
     fun permute_bd_cinfinite_tac _ = rtac (bd_cinfinite_of_bnf bnf) 1;
     val permute_set_bd_tacs = permute (map (fn thm => fn _ => rtac thm 1) (set_bd_of_bnf bnf));
 
     val permute_in_alt_thm =
-      if ! quick_and_dirty then
-        no_thm
-      else
-        let
-          val permute_in = mk_in Asets permute_sets T;
-          val permute_in_alt = mk_in (permute_rev Asets) bnf_sets T;
-          val goal = fold_rev Logic.all Asets (mk_Trueprop_eq (permute_in, permute_in_alt));
-        in
-          Skip_Proof.prove lthy [] [] goal (K (mk_permute_in_alt_tac src dest))
-          |> Thm.close_derivation
-        end;
+      let
+        val permute_in = mk_in Asets permute_sets T;
+        val permute_in_alt = mk_in (permute_rev Asets) bnf_sets T;
+        val goal = fold_rev Logic.all Asets (mk_Trueprop_eq (permute_in, permute_in_alt));
+      in
+        Skip_Proof.prove lthy [] [] goal (K (mk_permute_in_alt_tac src dest))
+        |> Thm.close_derivation
+      end;
 
     fun permute_in_bd_tac _ =
       mk_permute_in_bd_tac src dest permute_in_alt_thm (in_bd_of_bnf bnf)
         (bd_Card_order_of_bnf bnf);
     fun permute_map_wpull_tac _ =