# 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;