# HG changeset patch
# User blanchet
# Date 1307385394 -7200
# Node ID d4f347508cd4c77d1a77773ee5196b1c11b425e8
# Parent  29b55f292e0bc12df8cf82b3a2ef2aba4fdcfa36
clean up unnecessary machinery -- helpers work also with monomorphic type encodings

diff -r 29b55f292e0b -r d4f347508cd4 src/HOL/Tools/Metis/metis_tactics.ML
--- a/src/HOL/Tools/Metis/metis_tactics.ML	Mon Jun 06 20:36:34 2011 +0200
+++ b/src/HOL/Tools/Metis/metis_tactics.ML	Mon Jun 06 20:36:34 2011 +0200
@@ -71,9 +71,6 @@
   end
   |> Meson.make_meta_clause
 
-(* FIXME: implement using "hol_clause_from_metis ctxt sym_tab mth" *)
-fun specialize_helper mth ith = ith
-
 val clause_params =
   {ordering = Metis_KnuthBendixOrder.default,
    orderLiterals = Metis_Clause.UnsignedLiteralOrder,
@@ -109,9 +106,6 @@
         prepare_metis_problem ctxt mode type_sys cls ths
       fun get_isa_thm mth Isa_Reflexive_or_Trivial =
           reflexive_or_trivial_from_metis ctxt sym_tab mth
-        | get_isa_thm mth (Isa_Helper ith) =
-          ith |> should_specialize_helper (the type_sys) (prop_of ith)
-                 ? specialize_helper mth
         | get_isa_thm _ (Isa_Raw ith) = ith
       val axioms = axioms |> map (fn (mth, ith) => (mth, get_isa_thm mth ith))
       val _ = trace_msg ctxt (fn () => "CLAUSES GIVEN TO METIS")
diff -r 29b55f292e0b -r d4f347508cd4 src/HOL/Tools/Metis/metis_translate.ML
--- a/src/HOL/Tools/Metis/metis_translate.ML	Mon Jun 06 20:36:34 2011 +0200
+++ b/src/HOL/Tools/Metis/metis_translate.ML	Mon Jun 06 20:36:34 2011 +0200
@@ -16,7 +16,6 @@
 
   datatype isa_thm =
     Isa_Reflexive_or_Trivial |
-    Isa_Helper of thm |
     Isa_Raw of thm
 
   type metis_problem =
@@ -242,7 +241,6 @@
 
 datatype isa_thm =
   Isa_Reflexive_or_Trivial |
-  Isa_Helper of thm |
   Isa_Raw of thm
 
 type metis_problem =
@@ -328,9 +326,9 @@
      else if String.isPrefix helper_prefix ident then
        case space_explode "_" ident  of
          _ :: const :: j :: _ =>
-         Isa_Helper (nth (AList.lookup (op =) helper_table const |> the |> snd)
-                         (the (Int.fromString j) - 1)
-                     |> prepare_helper)
+         Isa_Raw (nth (AList.lookup (op =) helper_table const |> the |> snd)
+                      (the (Int.fromString j) - 1)
+                  |> prepare_helper)
        | _ => raise Fail ("malformed helper identifier " ^ quote ident)
      else case try (unprefix conjecture_prefix) ident of
        SOME s =>