src/HOL/Tools/Metis/metis_reconstruct.ML
changeset 42337 fef417b12f38
parent 42333 23bb0784b5d0
child 42339 0e5d1e5e1177
     1.1 --- a/src/HOL/Tools/Metis/metis_reconstruct.ML	Thu Apr 14 11:24:04 2011 +0200
     1.2 +++ b/src/HOL/Tools/Metis/metis_reconstruct.ML	Thu Apr 14 11:24:04 2011 +0200
     1.3 @@ -169,6 +169,13 @@
     1.4  fun hol_term_from_metis_FT ctxt new_skolem_var_count fol_tm =
     1.5    let val _ = trace_msg ctxt (fn () => "hol_term_from_metis_FT: " ^
     1.6                                         Metis_Term.toString fol_tm)
     1.7 +      fun do_const c =
     1.8 +        let val c = c |> invert_const in
     1.9 +          if String.isPrefix new_skolem_const_prefix c then
    1.10 +            Var ((new_skolem_var_name_from_const c, 1), dummyT)
    1.11 +          else
    1.12 +            Const (c, dummyT)
    1.13 +        end
    1.14        fun cvt (Metis_Term.Fn ("ti", [Metis_Term.Var v, _])) =
    1.15               (case strip_prefix_and_unascii schematic_var_prefix v of
    1.16                    SOME w =>  mk_var(w, dummyT)
    1.17 @@ -177,7 +184,7 @@
    1.18              Const (@{const_name HOL.eq}, HOLogic.typeT)
    1.19          | cvt (Metis_Term.Fn ("ti", [Metis_Term.Fn (x,[]), ty])) =
    1.20             (case strip_prefix_and_unascii const_prefix x of
    1.21 -                SOME c => Const (invert_const c, dummyT)
    1.22 +                SOME c => do_const c
    1.23                | NONE => (*Not a constant. Is it a fixed variable??*)
    1.24              case strip_prefix_and_unascii fixed_var_prefix x of
    1.25                  SOME v => Free (v, hol_type_from_metis_term ctxt ty)
    1.26 @@ -191,7 +198,7 @@
    1.27              list_comb(Const (@{const_name HOL.eq}, HOLogic.typeT), map cvt [tm1,tm2])
    1.28          | cvt (t as Metis_Term.Fn (x, [])) =
    1.29             (case strip_prefix_and_unascii const_prefix x of
    1.30 -                SOME c => Const (invert_const c, dummyT)
    1.31 +                SOME c => do_const c
    1.32                | NONE => (*Not a constant. Is it a fixed variable??*)
    1.33              case strip_prefix_and_unascii fixed_var_prefix x of
    1.34                  SOME v => Free (v, dummyT)