# HG changeset patch
# User smolkas
# Date 1357156352 -3600
# Node ID 027c09d7f6ec1ff2a52e9f88baa23506394c1ab4
# Parent  f5c217474eca54e2075836ae629724c922328421
removed duplicate code

diff -r f5c217474eca -r 027c09d7f6ec src/HOL/Tools/Sledgehammer/sledgehammer_shrink.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_shrink.ML	Wed Jan 02 20:35:49 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_shrink.ML	Wed Jan 02 20:52:32 2013 +0100
@@ -125,38 +125,29 @@
       (* TODO: add "Obtain" case *)
       fun try_metis timeout (succedent, Prove (_, _, t, byline)) =
         if not preplay then K (SOME Time.zeroTime) else
-        (case byline of
-          By_Metis fact_names =>
-            let
-              val facts = resolve_fact_names fact_names
-              val goal =
-                Goal.prove (Config.put Metis_Tactic.verbose debug ctxt) [] [] t
-              fun tac {context = ctxt, prems = _} =
-                Metis_Tactic.metis_tac [type_enc] lam_trans ctxt facts 1
-            in
-              take_time timeout (fn () => goal tac)
-            end
-        | Case_Split (cases, fact_names) =>
-            let
-              val make_thm = Skip_Proof.make_thm (Proof_Context.theory_of ctxt)
-              val facts =
-                resolve_fact_names fact_names
-                  @ (case the succedent of
-                      Assume (_, t) => make_thm t
-                    | Obtain (_, _, _, t, _) => make_thm t
-                    | Prove (_, _, t, _) => make_thm t
-                    | _ => error "Internal error: unexpected succedent of case split")
-                  :: map (hd #> (fn Assume (_, a) => Logic.mk_implies (a, t)
-                                  | _ => error "Internal error: malformed case split")
-                             #> Skip_Proof.make_thm (Proof_Context.theory_of ctxt))
-                         cases
-              val goal =
-                Goal.prove (Config.put Metis_Tactic.verbose debug ctxt) [] [] t
-              fun tac {context = ctxt, prems = _} =
-                Metis_Tactic.metis_tac [type_enc] lam_trans ctxt facts 1
-            in
-              take_time timeout (fn () => goal tac)
-            end)
+        let
+          val make_thm = Skip_Proof.make_thm (Proof_Context.theory_of ctxt)
+          val facts =
+            (case byline of
+              By_Metis fact_names => resolve_fact_names fact_names
+            | Case_Split (cases, fact_names) =>
+              resolve_fact_names fact_names
+                @ (case the succedent of
+                    Assume (_, t) => make_thm t
+                  | Obtain (_, _, _, t, _) => make_thm t
+                  | Prove (_, _, t, _) => make_thm t
+                  | _ => error "Internal error: unexpected succedent of case split")
+                :: map (hd #> (fn Assume (_, a) => Logic.mk_implies (a, t)
+                                | _ => error "Internal error: malformed case split")
+                           #> make_thm)
+                     cases)
+          val goal =
+            Goal.prove (Config.put Metis_Tactic.verbose debug ctxt) [] [] t
+          fun tac {context = ctxt, prems = _} =
+            Metis_Tactic.metis_tac [type_enc] lam_trans ctxt facts 1
+        in
+          take_time timeout (fn () => goal tac)
+        end
         | try_metis _ _  = K (SOME Time.zeroTime)
 
       val try_metis_quietly = the_default NONE oo try oo try_metis