# HG changeset patch
# User blanchet
# Date 1305793453 -7200
# Node ID 3bb63850488b1d29d2411798e9645f83d8a32402
# Parent  c8709be8a40f5e349da6ce881c436353c9e3622d
removed "poly_tags_light_bang" since highly unsound

diff -r c8709be8a40f -r 3bb63850488b src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Thu May 19 10:24:13 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Thu May 19 10:24:13 2011 +0200
@@ -127,20 +127,21 @@
                   | NONE => (NONE, s))
   |> (fn (poly, (level, (heaviness, core))) =>
          case (core, (poly, level, heaviness)) of
-           ("simple_types", (NONE, level, NONE)) => Simple_Types level
-         | ("preds", (SOME Polymorphic, level, _)) =>
+           ("simple_types", (NONE, _, NONE)) => Simple_Types level
+         | ("preds", (SOME Polymorphic, _, _)) =>
            if level = All_Types then
              Preds (Polymorphic, level, heaviness |> the_default Light)
            else
              raise Same.SAME
-         | ("preds", (SOME poly, level, _)) =>
+         | ("preds", (SOME poly, _, _)) =>
            Preds (poly, level, heaviness |> the_default Light)
-         | ("tags", (SOME Polymorphic, level, _)) =>
-           if level = All_Types orelse level = Finite_Types then
-             Tags (Polymorphic, level, heaviness |> the_default Light)
-           else
-             raise Same.SAME
-         | ("tags", (SOME poly, level, _)) =>
+         | ("tags", (SOME Polymorphic, All_Types, _)) =>
+           Tags (Polymorphic, All_Types, heaviness |> the_default Light)
+         | ("tags", (SOME Polymorphic, Finite_Types, _)) =>
+           if heaviness = SOME Light then raise Same.SAME
+           else Tags (Polymorphic, Finite_Types, Heavy)
+         | ("tags", (SOME Polymorphic, _, _)) => raise Same.SAME
+         | ("tags", (SOME poly, _, _)) =>
            Tags (poly, level, heaviness |> the_default Light)
          | ("args", (SOME poly, All_Types (* naja *), NONE)) =>
            Preds (poly, Const_Arg_Types, Light)