1.1 --- a/src/HOL/Tools/ATP/atp_problem.ML	Thu May 12 15:29:19 2011 +0200
     1.2 +++ b/src/HOL/Tools/ATP/atp_problem.ML	Thu May 12 15:29:19 2011 +0200
     1.3 @@ -171,6 +171,7 @@
     1.4        | keep (c :: cs) = c :: keep cs
     1.5    in String.explode #> rev #> keep #> rev #> String.implode end
     1.6  
     1.7 +(* Long names can slow down the ATPs. *)
     1.8  val max_readable_name_size = 20
     1.9  
    1.10  (* "op" is also reserved, to avoid the unreadable "op_1", "op_2", etc., in the

     2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML	Thu May 12 15:29:19 2011 +0200
     2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML	Thu May 12 15:29:19 2011 +0200
     2.3 @@ -357,7 +357,9 @@
     2.4                list_comb (Const (@{const_name HOL.eq}, HOLogic.typeT), ts)
     2.5            end
     2.6          | SOME s =>
     2.7 -          let val (s', mangled_us) = s |> unmangled_const |>> invert_const in
     2.8 +          let
     2.9 +            val ((s', s), mangled_us) = s |> unmangled_const |>> `invert_const
    2.10 +          in
    2.11              if s' = type_tag_name then
    2.12                case mangled_us @ us of
    2.13                  [typ_u, term_u] =>
    2.14 @@ -380,14 +382,12 @@
    2.15                  val term_ts = map (aux NONE []) term_us
    2.16                  val extra_ts = map (aux NONE []) extra_us
    2.17                  val T =
    2.18 -                  case opt_T of
    2.19 -                    SOME T => map fastype_of term_ts ---> T
    2.20 -                  | NONE =>
    2.21 -                    if num_type_args thy s' = length type_us then
    2.22 -                      Sign.const_instance thy
    2.23 -                          (s', map (typ_from_fo_term tfrees) type_us)
    2.24 -                    else
    2.25 -                      HOLogic.typeT
    2.26 +                  if num_type_args thy s' = length type_us then
    2.27 +                    Sign.const_instance thy
    2.28 +                        (s', map (typ_from_fo_term tfrees) type_us)
    2.29 +                  else case opt_T of
    2.30 +                    SOME T => map fastype_of (term_ts @ extra_ts) ---> T
    2.31 +                  | NONE => HOLogic.typeT
    2.32                  val s' = s' |> unproxify_const
    2.33                in list_comb (Const (s', T), term_ts @ extra_ts) end
    2.34            end
    2.35 @@ -424,14 +424,17 @@
    2.36     (@{const_name Meson.COMBC}, @{thm Meson.COMBC_def_raw}),
    2.37     (@{const_name Meson.COMBS}, @{thm Meson.COMBS_def_raw})]
    2.38  
    2.39 -fun uncombine_term (t1 $ t2) = betapply (pairself uncombine_term (t1, t2))
    2.40 -  | uncombine_term (Abs (s, T, t')) = Abs (s, T, uncombine_term t')
    2.41 -  | uncombine_term (t as Const (x as (s, _))) =
    2.42 -    (case AList.lookup (op =) combinator_table s of
    2.43 -       SOME thm => thm |> prop_of |> specialize_type @{theory} x
    2.44 -                       |> Logic.dest_equals |> snd
    2.45 -     | NONE => t)
    2.46 -  | uncombine_term t = t
    2.47 +fun uncombine_term thy =
    2.48 +  let
    2.49 +    fun aux (t1 $ t2) = betapply (pairself aux (t1, t2))
    2.50 +      | aux (Abs (s, T, t')) = Abs (s, T, aux t')
    2.51 +      | aux (t as Const (x as (s, _))) =
    2.52 +        (case AList.lookup (op =) combinator_table s of
    2.53 +           SOME thm => thm |> prop_of |> specialize_type thy x
    2.54 +                           |> Logic.dest_equals |> snd
    2.55 +         | NONE => t)
    2.56 +      | aux t = t
    2.57 +  in aux end
    2.58  
    2.59  (* Update schematic type variables with detected sort constraints. It's not
    2.60     totally clear whether this code is necessary. *)
    2.61 @@ -487,8 +490,8 @@
    2.62  
    2.63  fun check_formula ctxt =
    2.64    Type.constraint HOLogic.boolT
    2.65 -  #> Syntax.check_term (Proof_Context.set_mode Proof_Context.mode_schematic ctxt)
    2.66 -
    2.67 +  #> Syntax.check_term
    2.68 +         (Proof_Context.set_mode Proof_Context.mode_schematic ctxt)
    2.69  
    2.70  (**** Translation of TSTP files to Isar Proofs ****)
    2.71  
    2.72 @@ -505,7 +508,7 @@
    2.73        val t2 = prop_from_formula thy sym_tab tfrees phi2
    2.74        val (t1, t2) =
    2.75          HOLogic.eq_const HOLogic.typeT $ t1 $ t2
    2.76 -        |> unvarify_args |> uncombine_term |> check_formula ctxt
    2.77 +        |> unvarify_args |> uncombine_term thy |> check_formula ctxt
    2.78          |> HOLogic.dest_eq
    2.79      in
    2.80        (Definition (name, t1, t2),
    2.81 @@ -515,7 +518,7 @@
    2.82      let
    2.83        val thy = Proof_Context.theory_of ctxt
    2.84        val t = u |> prop_from_formula thy sym_tab tfrees
    2.85 -                |> uncombine_term |> check_formula ctxt
    2.86 +                |> uncombine_term thy |> check_formula ctxt
    2.87      in
    2.88        (Inference (name, t, deps),
    2.89         fold Variable.declare_term (OldTerm.term_frees t) ctxt)
    2.90 @@ -910,10 +913,10 @@
    2.91  
    2.92  fun string_for_proof ctxt0 i n =
    2.93    let
    2.94 -    val ctxt = ctxt0
    2.95 -      |> Config.put show_free_types false
    2.96 -      |> Config.put show_types true
    2.97 -      |> Config.put show_sorts true
    2.98 +    val ctxt =
    2.99 +      ctxt0 |> Config.put show_free_types false
   2.100 +            |> Config.put show_types true
   2.101 +            |> Config.put show_sorts true
   2.102      fun fix_print_mode f x =
   2.103        Print_Mode.setmp (filter (curry (op =) Symbol.xsymbolsN)
   2.104                                 (print_mode_value ())) f x

     3.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Thu May 12 15:29:19 2011 +0200
     3.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Thu May 12 15:29:19 2011 +0200
     3.3 @@ -269,7 +269,8 @@
     3.4  
     3.5  fun generic_mangled_type_name f (ATerm (name, [])) = f name
     3.6    | generic_mangled_type_name f (ATerm (name, tys)) =
     3.7 -    f name ^ "(" ^ commas (map (generic_mangled_type_name f) tys) ^ ")"
     3.8 +    f name ^ "(" ^ space_implode "," (map (generic_mangled_type_name f) tys)
     3.9 +    ^ ")"
    3.10  val mangled_type_name =
    3.11    fo_term_from_typ
    3.12    #> (fn ty => (make_tff_type (generic_mangled_type_name fst ty),