# HG changeset patch
# User blanchet
# Date 1431173410 -7200
# Node ID 35153674570483c6a5107e00d07bbb63a1f4eeae
# Parent  2a9bc6447779ec9cd61d7dd4e05eee2a196597d1
took out unreliable 'blast' from tactic altogether

diff -r 2a9bc6447779 -r 351536745704 src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML
--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Fri May 08 16:14:02 2015 +0200
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Sat May 09 14:10:10 2015 +0200
@@ -397,7 +397,13 @@
 
     val ctrs0 = map (prep_term no_defs_lthy) raw_ctrs;
 
-    val Type (fcT_name, As0) = body_type (fastype_of (hd ctrs0));
+    val (fcT_name, As0) =
+      (case body_type (fastype_of (hd ctrs0)) of
+        Type T' => T'
+      | _ => error "Expected type constructor in body type of constructor");
+    val _ = forall ((fn Type (T_name, _) => T_name = fcT_name | _ => false) o body_type
+      o fastype_of) (tl ctrs0) orelse error "Constructors not constructing same type";
+
     val fc_b_name = Long_Name.base_name fcT_name;
     val fc_b = Binding.name fc_b_name;
 
@@ -675,7 +681,7 @@
 
     val goalss = [exhaust_goal] :: inject_goalss @ half_distinct_goalss;
 
-    fun after_qed (thmss0 as [exhaust_thm] :: thmss) lthy =
+    fun after_qed ([exhaust_thm] :: thmss) lthy =
       let
         val ((inject_thms, inject_thmss), half_distinct_thmss) = chop n thmss |>> `flat;
 
diff -r 2a9bc6447779 -r 351536745704 src/HOL/Tools/Ctr_Sugar/ctr_sugar_tactics.ML
--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar_tactics.ML	Fri May 08 16:14:02 2015 +0200
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar_tactics.ML	Sat May 09 14:10:10 2015 +0200
@@ -44,9 +44,6 @@
 
 val meta_mp = @{thm meta_mp};
 
-fun clean_blast_depth_tac ctxt depth =
-  depth_tac (put_claset (claset_of @{theory_context HOL}) ctxt) depth;
-
 fun select_prem_tac n tac k = DETERM o (EVERY' [REPEAT_DETERM_N (k - 1) o etac thin_rl,
   tac, REPEAT_DETERM_N (n - k) o etac thin_rl]);
 
@@ -176,7 +173,10 @@
     ALLGOALS (fn k => (hyp_subst_tac ctxt THEN'
        simp_tac (ss_only (@{thms simp_thms} @ cases @ nth selss (k - 1) @ nth injectss (k - 1) @
          flat (nth distinctsss (k - 1))) ctxt)) k) THEN
-    ALLGOALS (clean_blast_depth_tac ctxt depth)
+    ALLGOALS (etac thin_rl THEN' rtac iffI THEN'
+      REPEAT_DETERM o rtac allI THEN' rtac impI THEN' REPEAT_DETERM o etac conjE THEN'
+      hyp_subst_tac ctxt THEN' atac THEN' REPEAT_DETERM o etac allE THEN' etac impE THEN'
+      REPEAT_DETERM o (rtac conjI THEN' rtac refl) THEN' rtac refl THEN' atac)
   end;
 
 val split_asm_thms = @{thms imp_conv_disj de_Morgan_conj de_Morgan_disj not_not not_ex};