# HG changeset patch
# User blanchet
# Date 1286359315 -7200
# Node ID 12eb8fe15b004806632a70d5cf94835bab9c742d
# Parent  88c9aa5666de7c0c15883bf30b25e10d6f11cb20
added a few FIXMEs

diff -r 88c9aa5666de -r 12eb8fe15b00 src/HOL/Tools/Metis/metis_tactics.ML
--- a/src/HOL/Tools/Metis/metis_tactics.ML	Tue Oct 05 12:50:45 2010 +0200
+++ b/src/HOL/Tools/Metis/metis_tactics.ML	Wed Oct 06 12:01:55 2010 +0200
@@ -57,6 +57,9 @@
    models = []}
 val resolution_params = {active = active_params, waiting = waiting_params}
 
+(* FIXME ### GET RID OF skolem WRAPPER by looking at substitution *)
+
+(* FIXME ### try cterm_instantiate *)
 fun instantiate_theorem thy inst th =
   let
     val tyenv = Vartab.empty |> fold (Type.raw_unify o pairself fastype_of) inst
@@ -80,6 +83,7 @@
    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
@@ -161,8 +165,8 @@
         |> map_filter (fn (ax_no', (_, (_, tsubst))) =>
                           if ax_no' = ax_no then
                             tsubst |> filter (in_right_cluster
-                                               o fst o fst o dest_Var o fst)
-                                    |> map snd |> SOME
+                                              o fst o fst o dest_Var o fst)
+                                   |> map snd |> SOME
                            else
                              NONE)
       val n = length cluster_substs