1.1 --- a/src/HOL/Tools/Metis/metis_reconstruct.ML	Sun May 01 18:37:25 2011 +0200
     1.2 +++ b/src/HOL/Tools/Metis/metis_reconstruct.ML	Sun May 01 18:37:25 2011 +0200
     1.3 @@ -123,7 +123,7 @@
     1.4              case strip_prefix_and_unascii const_prefix a of
     1.5                  SOME b =>
     1.6                    let
     1.7 -                    val c = invert_const b
     1.8 +                    val c = b |> invert_const |> unproxify_const
     1.9                      val ntypes = num_type_args thy c
    1.10                      val nterms = length ts - ntypes
    1.11                      val tts = map tm_to_tt ts
    1.12 @@ -168,7 +168,7 @@
    1.13    let val _ = trace_msg ctxt (fn () => "hol_term_from_metis_FT: " ^
    1.14                                         Metis_Term.toString fol_tm)
    1.15        fun do_const c =
    1.16 -        let val c = c |> invert_const in
    1.17 +        let val c = c |> invert_const |> unproxify_const in
    1.18            if String.isPrefix new_skolem_const_prefix c then
    1.19              Var ((new_skolem_var_name_from_const c, 1), dummyT)
    1.20            else

     2.1 --- a/src/HOL/Tools/Metis/metis_translate.ML	Sun May 01 18:37:25 2011 +0200
     2.2 +++ b/src/HOL/Tools/Metis/metis_translate.ML	Sun May 01 18:37:25 2011 +0200
     2.3 @@ -43,9 +43,9 @@
     2.4    val type_const_prefix: string
     2.5    val class_prefix: string
     2.6    val new_skolem_const_prefix : string
     2.7 -  val metis_proxies : (string * (string * string)) list
     2.8 -  val safe_invert_const: string -> string
     2.9 +  val proxify_const : string -> (string * string) option
    2.10    val invert_const: string -> string
    2.11 +  val unproxify_const: string -> string
    2.12    val ascii_of: string -> string
    2.13    val unascii_of: string -> string
    2.14    val strip_prefix_and_unascii: string -> string -> string option
    2.15 @@ -104,13 +104,16 @@
    2.16  fun union_all xss = fold (union (op =)) xss []
    2.17  
    2.18  val metis_proxies =
    2.19 -  [("c_False", ("fFalse", @{const_name Metis.fFalse})),
    2.20 -   ("c_True", ("fTrue", @{const_name Metis.fTrue})),
    2.21 -   ("c_Not", ("fNot", @{const_name Metis.fNot})),
    2.22 -   ("c_conj", ("fconj", @{const_name Metis.fconj})),
    2.23 -   ("c_disj", ("fdisj", @{const_name Metis.fdisj})),
    2.24 -   ("c_implies", ("fimplies", @{const_name Metis.fimplies})),
    2.25 -   ("equal", ("fequal", @{const_name Metis.fequal}))]
    2.26 +  [("c_False", (@{const_name False}, ("fFalse", @{const_name Metis.fFalse}))),
    2.27 +   ("c_True", (@{const_name True}, ("fTrue", @{const_name Metis.fTrue}))),
    2.28 +   ("c_Not", (@{const_name Not}, ("fNot", @{const_name Metis.fNot}))),
    2.29 +   ("c_conj", (@{const_name conj}, ("fconj", @{const_name Metis.fconj}))),
    2.30 +   ("c_disj", (@{const_name disj}, ("fdisj", @{const_name Metis.fdisj}))),
    2.31 +   ("c_implies", (@{const_name implies},
    2.32 +                  ("fimplies", @{const_name Metis.fimplies}))),
    2.33 +   ("equal", (@{const_name HOL.eq}, ("fequal", @{const_name Metis.fequal})))]
    2.34 +
    2.35 +val proxify_const = AList.lookup (op =) metis_proxies #> Option.map snd
    2.36  
    2.37  (* Readable names for the more common symbolic functions. Do not mess with the
    2.38     table unless you know what you are doing. *)
    2.39 @@ -130,25 +133,20 @@
    2.40     (@{const_name Meson.COMBK}, "COMBK"),
    2.41     (@{const_name Meson.COMBB}, "COMBB"),
    2.42     (@{const_name Meson.COMBC}, "COMBC"),
    2.43 -   (@{const_name Meson.COMBS}, "COMBS")] @
    2.44 -   (metis_proxies |> map (swap o snd))
    2.45 +   (@{const_name Meson.COMBS}, "COMBS")]
    2.46    |> Symtab.make
    2.47 +  |> fold (Symtab.update o swap o snd o snd) metis_proxies
    2.48  
    2.49 -(* Invert the table of translations between Isabelle and ATPs. *)
    2.50 -val const_trans_table_safe_inv =
    2.51 +(* Invert the table of translations between Isabelle and Metis. *)
    2.52 +val const_trans_table_inv =
    2.53    const_trans_table |> Symtab.dest |> map swap |> Symtab.make
    2.54 -val const_trans_table_inv =
    2.55 -  const_trans_table_safe_inv
    2.56 -  |> fold Symtab.update [("fFalse", @{const_name False}),
    2.57 -                         ("fTrue", @{const_name True}),
    2.58 -                         ("fNot", @{const_name Not}),
    2.59 -                         ("fconj", @{const_name conj}),
    2.60 -                         ("fdisj", @{const_name disj}),
    2.61 -                         ("fimplies", @{const_name implies}),
    2.62 -                         ("fequal", @{const_name HOL.eq})]
    2.63 +val const_trans_table_unprox =
    2.64 +  Symtab.empty
    2.65 +  |> fold (fn (_, (isa, (_, meson))) => Symtab.update (meson, isa))
    2.66 +          metis_proxies
    2.67  
    2.68 -val safe_invert_const = perhaps (Symtab.lookup const_trans_table_safe_inv)
    2.69  val invert_const = perhaps (Symtab.lookup const_trans_table_inv)
    2.70 +val unproxify_const = perhaps (Symtab.lookup const_trans_table_unprox)
    2.71  
    2.72  (*Escaping of special characters.
    2.73    Alphanumeric characters are left unchanged.
    2.74 @@ -398,41 +396,32 @@
    2.75  (* Converts a term (with combinators) into a combterm. Also accumulates sort
    2.76     infomation. *)
    2.77  fun combterm_from_term thy bs (P $ Q) =
    2.78 -      let
    2.79 -        val (P', P_atomics_Ts) = combterm_from_term thy bs P
    2.80 -        val (Q', Q_atomics_Ts) = combterm_from_term thy bs Q
    2.81 -      in (CombApp (P', Q'), union (op =) P_atomics_Ts Q_atomics_Ts) end
    2.82 +    let
    2.83 +      val (P', P_atomics_Ts) = combterm_from_term thy bs P
    2.84 +      val (Q', Q_atomics_Ts) = combterm_from_term thy bs Q
    2.85 +    in (CombApp (P', Q'), union (op =) P_atomics_Ts Q_atomics_Ts) end
    2.86    | combterm_from_term thy _ (Const (c, T)) =
    2.87 -      let
    2.88 -        val tvar_list =
    2.89 -          (if String.isPrefix old_skolem_const_prefix c then
    2.90 -             [] |> Term.add_tvarsT T |> map TVar
    2.91 -           else
    2.92 -             (c, T) |> Sign.const_typargs thy)
    2.93 -        val c' = CombConst (`make_fixed_const c, T, tvar_list)
    2.94 -      in (c', atyps_of T) end
    2.95 +    let
    2.96 +      val tvar_list =
    2.97 +        (if String.isPrefix old_skolem_const_prefix c then
    2.98 +           [] |> Term.add_tvarsT T |> map TVar
    2.99 +         else
   2.100 +           (c, T) |> Sign.const_typargs thy)
   2.101 +      val c' = CombConst (`make_fixed_const c, T, tvar_list)
   2.102 +    in (c', atyps_of T) end
   2.103    | combterm_from_term _ _ (Free (v, T)) =
   2.104 -      let
   2.105 -        val at = atyps_of T
   2.106 -        val v' = CombConst (`make_fixed_var v, T, [])
   2.107 -      in (v', atyps_of T) end
   2.108 +    (CombConst (`make_fixed_var v, T, []), atyps_of T)
   2.109    | combterm_from_term _ _ (Var (v as (s, _), T)) =
   2.110 -    let
   2.111 -      val v' =
   2.112 -        if String.isPrefix Meson_Clausify.new_skolem_var_prefix s then
   2.113 -          let
   2.114 -            val Ts = T |> strip_type |> swap |> op ::
   2.115 -            val s' = new_skolem_const_name s (length Ts)
   2.116 -          in CombConst (`make_fixed_const s', T, Ts) end
   2.117 -        else
   2.118 -          CombVar ((make_schematic_var v, s), T)
   2.119 -    in (v', atyps_of T) end
   2.120 +    (if String.isPrefix Meson_Clausify.new_skolem_var_prefix s then
   2.121 +       let
   2.122 +         val Ts = T |> strip_type |> swap |> op ::
   2.123 +         val s' = new_skolem_const_name s (length Ts)
   2.124 +       in CombConst (`make_fixed_const s', T, Ts) end
   2.125 +     else
   2.126 +       CombVar ((make_schematic_var v, s), T), atyps_of T)
   2.127    | combterm_from_term _ bs (Bound j) =
   2.128 -      let
   2.129 -        val (s, T) = nth bs j
   2.130 -        val ts = atyps_of T
   2.131 -        val v' = CombConst (`make_bound_var s, T, [])
   2.132 -      in (v', atyps_of T) end
   2.133 +    nth bs j
   2.134 +    |> (fn (s, T) => (CombConst (`make_bound_var s, T, []), atyps_of T))
   2.135    | combterm_from_term _ _ (Abs _) = raise Fail "HOL clause: Abs"
   2.136  
   2.137  fun predicate_of thy ((@{const Not} $ P), pos) = predicate_of thy (P, not pos)

     3.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML	Sun May 01 18:37:25 2011 +0200
     3.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML	Sun May 01 18:37:25 2011 +0200
     3.3 @@ -383,6 +383,7 @@
     3.4                            (b, map (typ_from_fo_term tfrees) type_us)
     3.5                      else
     3.6                        HOLogic.typeT
     3.7 +                val b = unproxify_const b
     3.8                in list_comb (Const (b, T), term_ts @ extra_ts) end
     3.9            end
    3.10          | NONE => (* a free or schematic variable *)

     4.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Sun May 01 18:37:25 2011 +0200
     4.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Sun May 01 18:37:25 2011 +0200
     4.3 @@ -226,7 +226,7 @@
     4.4      fun aux top_level (CombApp (tm1, tm2)) =
     4.5          CombApp (aux top_level tm1, aux false tm2)
     4.6        | aux top_level (CombConst (name as (s, s'), ty, ty_args)) =
     4.7 -        (case AList.lookup (op =) metis_proxies s of
     4.8 +        (case proxify_const s of
     4.9             SOME proxy_base =>
    4.10             if top_level then
    4.11               (case s of
    4.12 @@ -419,8 +419,7 @@
    4.13             t |> (general_type_arg_policy type_sys = Mangled_Types andalso
    4.14                   not (null (Term.hidden_polymorphism t)))
    4.15                  ? (case typ of
    4.16 -                     SOME T =>
    4.17 -                     specialize_type thy (safe_invert_const unmangled_s, T)
    4.18 +                     SOME T => specialize_type thy (invert_const unmangled_s, T)
    4.19                     | NONE => I)
    4.20           end)
    4.21        fun make_facts eq_as_iff =
    4.22 @@ -477,7 +476,7 @@
    4.23          (case strip_prefix_and_unascii const_prefix s of
    4.24             NONE => (name, ty_args)
    4.25           | SOME s'' =>
    4.26 -           let val s'' = safe_invert_const s'' in
    4.27 +           let val s'' = invert_const s'' in
    4.28               case type_arg_policy type_sys s'' of
    4.29                 No_Type_Args => (name, [])
    4.30               | Mangled_Types => (mangled_const_name ty_args name, [])
    4.31 @@ -682,7 +681,7 @@
    4.32    | NONE =>
    4.33      case strip_prefix_and_unascii const_prefix s of
    4.34        SOME s =>
    4.35 -      let val s = s |> unmangled_const_name |> safe_invert_const in
    4.36 +      let val s = s |> unmangled_const_name |> invert_const in
    4.37          if s = predicator_base then 1
    4.38          else if s = explicit_app_base then 2
    4.39          else if s = type_pred_base then 1