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