# HG changeset patch
# User blanchet
# Date 1300985367 -3600
# Node ID a6725f293377fb89099c44354f475addd945f6ef
# Parent  ed1d40888b1b5b5e84a2402fd088416b04f86329
clean up new Skolemizer code -- some old hacks are no longer necessary

diff -r ed1d40888b1b -r a6725f293377 src/HOL/Tools/Metis/metis_reconstruct.ML
--- a/src/HOL/Tools/Metis/metis_reconstruct.ML	Thu Mar 24 17:49:27 2011 +0100
+++ b/src/HOL/Tools/Metis/metis_reconstruct.ML	Thu Mar 24 17:49:27 2011 +0100
@@ -585,50 +585,6 @@
 
 fun term_instantiate thy = cterm_instantiate o map (pairself (cterm_of thy))
 
-(* In principle, it should be sufficient to apply "assume_tac" to unify the
-   conclusion with one of the premises. However, in practice, this is unreliable
-   because of the mildly higher-order nature of the unification problems.
-   Typical constraints are of the form
-   "?SK_a_b_c_x SK_d_e_f_y ... SK_a_b_c_x ... SK_g_h_i_z =?= SK_a_b_c_x",
-   where the nonvariables are goal parameters. *)
-(* FIXME: ### try Pattern.match instead *)
-fun unify_first_prem_with_concl thy i th =
-  let
-    val goal = Logic.get_goal (prop_of th) i |> Envir.beta_eta_contract
-    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
-    fun add_terms tp inst =
-      if exists (pair_untyped_aconv tp) inst then inst
-      else tp :: map (apsnd (subst_atomic [tp])) inst
-    fun is_flex t =
-      case strip_comb t of
-        (Var _, args) => forall is_Bound args
-      | _ => false
-    fun unify_flex flex rigid =
-      case strip_comb flex of
-        (Var (z as (_, T)), args) =>
-        add_terms (Var z,
-          fold_rev (curry absdummy) (take (length args) (binder_types T)) rigid)
-      | _ => raise TERM ("unify_flex: expected flex", [flex])
-    fun unify_potential_flex comb atom =
-      if is_flex comb then unify_flex comb atom
-      else if is_Var atom then add_terms (atom, comb)
-      else raise TERM ("unify_potential_flex", [comb, atom])
-    fun unify_terms (t, u) =
-      case (t, u) of
-        (t1 $ t2, u1 $ u2) =>
-        if is_flex t then unify_flex t u
-        else if is_flex u then unify_flex u t
-        else fold unify_terms [(t1, u1), (t2, u2)]
-      | (_ $ _, _) => unify_potential_flex t u
-      | (_, _ $ _) => unify_potential_flex u t
-      | (Var _, _) => add_terms (t, u)
-      | (_, Var _) => add_terms (u, t)
-      | _ => if untyped_aconv t u then I else raise TERM ("unify_terms", [t, u])
-  in th |> term_instantiate thy (unify_terms (prem, concl) []) end
-
 val copy_prem = @{lemma "P ==> (P ==> P ==> Q) ==> Q" by fast}
 
 fun copy_prems_tac [] ns i =
@@ -730,16 +686,6 @@
   else
     let
       val thy = ProofContext.theory_of ctxt
-      (* distinguish variables with same name but different types *)
-      (* ### FIXME: needed? *)
-      val prems_imp_false' =
-        prems_imp_false |> try (forall_intr_vars #> gen_all)
-                        |> the_default prems_imp_false
-      val prems_imp_false =
-        if prop_of prems_imp_false aconv prop_of prems_imp_false' then
-          prems_imp_false
-        else
-          prems_imp_false'
       fun match_term p =
         let
           val (tyenv, tenv) =
@@ -832,7 +778,6 @@
               THEN ALLGOALS (fn i =>
                        rtac @{thm Meson.skolem_COMBK_I} i
                        THEN rotate_tac (rotation_for_subgoal i) i
-(*                       THEN PRIMITIVE (unify_first_prem_with_concl thy i)  FIXME: needed? *)
                        THEN assume_tac i)))
       handle ERROR _ =>
              error ("Cannot replay Metis proof in Isabelle:\n\
diff -r ed1d40888b1b -r a6725f293377 src/HOL/Tools/Metis/metis_translate.ML
--- a/src/HOL/Tools/Metis/metis_translate.ML	Thu Mar 24 17:49:27 2011 +0100
+++ b/src/HOL/Tools/Metis/metis_translate.ML	Thu Mar 24 17:49:27 2011 +0100
@@ -805,7 +805,7 @@
             val helper_ths =
               metis_helpers
               |> filter (is_used o fst)
-              |> maps (fn (c, (needs_full_types, thms)) =>
+              |> maps (fn (_, (needs_full_types, thms)) =>
                           if needs_full_types andalso mode <> FT then []
                           else map prepare_helper thms)
           in lmap |> fold (add_thm false) helper_ths end