# HG changeset patch
# User blanchet
# Date 1306916983 -7200
# Node ID 0c82e00ba63ec5f3ce93f5fb124a1130949d38de
# Parent  eb8ec21c9a4888dadf7e822f945b7c6a52758726
make sure no warnings are given for polymorphic facts where we use a monomorphic instance

diff -r eb8ec21c9a48 -r 0c82e00ba63e src/HOL/Tools/Metis/metis_reconstruct.ML
--- a/src/HOL/Tools/Metis/metis_reconstruct.ML	Wed Jun 01 10:29:43 2011 +0200
+++ b/src/HOL/Tools/Metis/metis_reconstruct.ML	Wed Jun 01 10:29:43 2011 +0200
@@ -20,7 +20,7 @@
   val hol_term_from_metis :
     mode -> int Symtab.table -> Proof.context -> Metis_Term.term -> term
   val lookth : (Metis_Thm.thm * 'a) list -> Metis_Thm.thm -> 'a
-  val untyped_aconv : term -> term -> bool
+  val untyped_aconv : term * term -> bool
   val replay_one_inference :
     Proof.context -> mode -> (string * term) list -> int Symtab.table
     -> Metis_Thm.thm * Metis_Proof.inference -> (Metis_Thm.thm * thm) list
@@ -379,22 +379,22 @@
   | simp_not_not t = t
 
 (* Match untyped terms. *)
-fun untyped_aconv (Const (a, _)) (Const(b, _)) = (a = b)
-  | untyped_aconv (Free (a, _)) (Free (b, _)) = (a = b)
-  | untyped_aconv (Var ((a, _), _)) (Var ((b, _), _)) =
-    (a = b) (* The index is ignored, for some reason. *)
-  | untyped_aconv (Bound i) (Bound j) = (i = j)
-  | untyped_aconv (Abs (_, _, t)) (Abs (_, _, u)) = untyped_aconv t u
-  | untyped_aconv (t1 $ t2) (u1 $ u2) =
-    untyped_aconv t1 u1 andalso untyped_aconv t2 u2
-  | untyped_aconv _ _ = false
+fun untyped_aconv (Const (a, _), Const(b, _)) = (a = b)
+  | untyped_aconv (Free (a, _), Free (b, _)) = (a = b)
+  | untyped_aconv (Var ((a, _), _), Var ((b, _), _)) = (a = b)
+  | untyped_aconv (Bound i, Bound j) = (i = j)
+  | untyped_aconv (Abs (_, _, t), Abs (_, _, u)) = untyped_aconv (t, u)
+  | untyped_aconv (t1 $ t2, u1 $ u2) =
+    untyped_aconv (t1, u1) andalso untyped_aconv (t2, u2)
+  | untyped_aconv _ = false
 
 (* Finding the relative location of an untyped term within a list of terms *)
 fun index_of_literal lit haystack =
   let
     val normalize = simp_not_not o Envir.eta_contract
     val match_lit =
-      HOLogic.dest_Trueprop #> normalize #> untyped_aconv (lit |> normalize)
+      HOLogic.dest_Trueprop #> normalize
+      #> curry untyped_aconv (lit |> normalize)
   in case find_index match_lit haystack of ~1 => raise Empty | n => n + 1 end
 
 (* Permute a rule's premises to move the i-th premise to the last position. *)
@@ -644,7 +644,7 @@
     else
       let
         val (prems0, concl) = th |> prop_of |> Logic.strip_horn
-        val prems = prems0 |> distinct (uncurry untyped_aconv)
+        val prems = prems0 |> distinct untyped_aconv
         val goal = Logic.list_implies (prems, concl)
       in
         if length prems = length prems0 then
@@ -692,7 +692,7 @@
     val prem = goal |> Logic.strip_assums_hyp |> hd
     val concl = goal |> Logic.strip_assums_concl
     fun pair_untyped_aconv (t1, t2) (u1, u2) =
-      untyped_aconv t1 u1 andalso untyped_aconv t2 u2
+      untyped_aconv (t1, u1) andalso untyped_aconv (t2, u2)
     fun add_terms tp inst =
       if exists (pair_untyped_aconv tp) inst then inst
       else tp :: map (apsnd (subst_atomic [tp])) inst
diff -r eb8ec21c9a48 -r 0c82e00ba63e src/HOL/Tools/Metis/metis_tactics.ML
--- a/src/HOL/Tools/Metis/metis_tactics.ML	Wed Jun 01 10:29:43 2011 +0200
+++ b/src/HOL/Tools/Metis/metis_tactics.ML	Wed Jun 01 10:29:43 2011 +0200
@@ -48,8 +48,10 @@
 
 fun is_false t = t aconv (HOLogic.mk_Trueprop HOLogic.false_const);
 
+(* Designed to work also with monomorphic instances of polymorphic theorems. *)
 fun have_common_thm ths1 ths2 =
-  exists (member Thm.eq_thm ths1) (map Meson.make_meta_clause ths2)
+  exists (member (untyped_aconv o pairself prop_of) ths1)
+         (map Meson.make_meta_clause ths2)
 
 (*Determining which axiom clauses are actually used*)
 fun used_axioms axioms (th, Metis_Proof.Axiom _) = SOME (lookth axioms th)
@@ -137,18 +139,24 @@
                 val result =
                   fold (replay_one_inference ctxt' mode old_skolems sym_tab)
                        proof axioms
-                and used = map_filter (used_axioms axioms) proof
+                val used = map_filter (used_axioms axioms) proof
                 val _ = trace_msg ctxt (fn () => "METIS COMPLETED...clauses actually used:")
                 val _ = app (fn th => trace_msg ctxt (fn () => Display.string_of_thm ctxt th)) used
-                val unused = th_cls_pairs |> map_filter (fn (name, (_, cls)) =>
-                  if have_common_thm used cls then NONE else SOME name)
+                val names = th_cls_pairs |> map fst
+                val used_names =
+                  th_cls_pairs
+                  |> map_filter (fn (name, (_, cls)) =>
+                                    if have_common_thm used cls then SOME name
+                                    else NONE)
+                val unused_names = names |> subtract (op =) used_names
             in
                 if not (null cls) andalso not (have_common_thm used cls) then
                   verbose_warning ctxt "The assumptions are inconsistent"
                 else
                   ();
-                if not (null unused) then
-                  verbose_warning ctxt ("Unused theorems: " ^ commas_quote unused)
+                if not (null unused_names) then
+                  "Unused theorems: " ^ commas_quote unused_names
+                  |> verbose_warning ctxt
                 else
                   ();
                 case result of