# HG changeset patch
# User blanchet
# Date 1302773044 -7200
# Node ID fef417b12f383c32e61d59ca83660a3931bf7556
# Parent  d63d43e858793ba226edf5a06359f617a746e12e
make new Skolemizer work also for "metisFT"

diff -r d63d43e85879 -r fef417b12f38 src/HOL/Tools/Metis/metis_reconstruct.ML
--- a/src/HOL/Tools/Metis/metis_reconstruct.ML	Thu Apr 14 11:24:04 2011 +0200
+++ b/src/HOL/Tools/Metis/metis_reconstruct.ML	Thu Apr 14 11:24:04 2011 +0200
@@ -169,6 +169,13 @@
 fun hol_term_from_metis_FT ctxt new_skolem_var_count fol_tm =
   let val _ = trace_msg ctxt (fn () => "hol_term_from_metis_FT: " ^
                                        Metis_Term.toString fol_tm)
+      fun do_const c =
+        let val c = c |> invert_const in
+          if String.isPrefix new_skolem_const_prefix c then
+            Var ((new_skolem_var_name_from_const c, 1), dummyT)
+          else
+            Const (c, dummyT)
+        end
       fun cvt (Metis_Term.Fn ("ti", [Metis_Term.Var v, _])) =
              (case strip_prefix_and_unascii schematic_var_prefix v of
                   SOME w =>  mk_var(w, dummyT)
@@ -177,7 +184,7 @@
             Const (@{const_name HOL.eq}, HOLogic.typeT)
         | cvt (Metis_Term.Fn ("ti", [Metis_Term.Fn (x,[]), ty])) =
            (case strip_prefix_and_unascii const_prefix x of
-                SOME c => Const (invert_const c, dummyT)
+                SOME c => do_const c
               | NONE => (*Not a constant. Is it a fixed variable??*)
             case strip_prefix_and_unascii fixed_var_prefix x of
                 SOME v => Free (v, hol_type_from_metis_term ctxt ty)
@@ -191,7 +198,7 @@
             list_comb(Const (@{const_name HOL.eq}, HOLogic.typeT), map cvt [tm1,tm2])
         | cvt (t as Metis_Term.Fn (x, [])) =
            (case strip_prefix_and_unascii const_prefix x of
-                SOME c => Const (invert_const c, dummyT)
+                SOME c => do_const c
               | NONE => (*Not a constant. Is it a fixed variable??*)
             case strip_prefix_and_unascii fixed_var_prefix x of
                 SOME v => Free (v, dummyT)