# HG changeset patch
# User paulson
# Date 1252339335 -3600
# Node ID b4d49a4f4436436bf7f74d6700d89a2abb177ff2
# Parent  88cd351ec5dc035c975a8ff35f398c080b5cf690
Fixed a few problems with the method metisFT

diff -r 88cd351ec5dc -r b4d49a4f4436 src/HOL/Tools/metis_tools.ML
--- a/src/HOL/Tools/metis_tools.ML	Mon Sep 07 16:25:12 2009 +0200
+++ b/src/HOL/Tools/metis_tools.ML	Mon Sep 07 17:02:15 2009 +0100
@@ -281,14 +281,15 @@
                (case Recon.strip_prefix ResClause.schematic_var_prefix v of
                     SOME w =>  mk_var(w, dummyT)
                   | NONE   => mk_var(v, dummyT))
+          | cvt (Metis.Term.Fn ("ti", [Metis.Term.Fn ("=",[]), ty])) = 
+              Const ("op =", HOLogic.typeT)
           | cvt (Metis.Term.Fn ("ti", [Metis.Term.Fn (x,[]), ty])) =
              (case Recon.strip_prefix ResClause.const_prefix x of
                   SOME c => Const (Recon.invert_const c, dummyT)
                 | NONE => (*Not a constant. Is it a fixed variable??*)
               case Recon.strip_prefix ResClause.fixed_var_prefix x of
                   SOME v => Free (v, fol_type_to_isa ctxt ty)
-                | NONE => if x = "=" then Const ("op =", HOLogic.typeT)
-                          else error ("fol_term_to_hol_FT bad constant: " ^ x))
+                | NONE => error ("fol_term_to_hol_FT bad constant: " ^ x))
           | cvt (Metis.Term.Fn ("ti", [Metis.Term.Fn (".",[tm1,tm2]), _])) =
               cvt tm1 $ cvt tm2
           | cvt (Metis.Term.Fn (".",[tm1,tm2])) = (*untyped application*)
@@ -723,7 +724,7 @@
 
   val metis_tac = metis_general_tac HO;
   val metisF_tac = metis_general_tac FO;
-  val metisFT_tac = metis_general_tac FO;
+  val metisFT_tac = metis_general_tac FT;
 
   fun method name mode comment = Method.setup name (Attrib.thms >> (fn ths => fn ctxt =>
     SIMPLE_METHOD' (CHANGED_PROP o metis_general_tac mode ctxt ths))) comment;