# HG changeset patch
# User traytel
# Date 1346849375 -7200
# Node ID f51ab68f882fcb8c4795f9419d1b2034a40bcf11
# Parent  4c507e92e4a24fd757b56d77379d15d0d393fd74
do not trivialize important internal theorem in quick_and_dirty mode

diff -r 4c507e92e4a2 -r f51ab68f882f src/HOL/Codatatype/Tools/bnf_comp.ML
--- a/src/HOL/Codatatype/Tools/bnf_comp.ML	Wed Sep 05 13:44:03 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_comp.ML	Wed Sep 05 14:49:35 2012 +0200
@@ -217,18 +217,15 @@
         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)
@@ -338,16 +335,13 @@
         (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)
@@ -446,16 +440,13 @@
         (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);
@@ -531,17 +522,14 @@
     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)