1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Mon Jul 26 17:17:59 2010 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Mon Jul 26 17:22:39 2010 +0200
     1.3 @@ -43,15 +43,6 @@
     1.4  fun is_conjecture_clause_number conjecture_shape num =
     1.5    index_in_shape num conjecture_shape >= 0
     1.6  
     1.7 -fun smart_lambda v t =
     1.8 -  Abs (case v of
     1.9 -         Const (s, _) =>
    1.10 -         List.last (space_explode skolem_infix (Long_Name.base_name s))
    1.11 -       | Var ((s, _), _) => s
    1.12 -       | Free (s, _) => s
    1.13 -       | _ => "", fastype_of v, abstract_over (v, t))
    1.14 -fun forall_of v t = HOLogic.all_const (fastype_of v) $ smart_lambda v t
    1.15 -
    1.16  fun negate_term (Const (@{const_name All}, T) $ Abs (s, T', t')) =
    1.17      Const (@{const_name Ex}, T) $ Abs (s, T', negate_term t')
    1.18    | negate_term (Const (@{const_name Ex}, T) $ Abs (s, T', t')) =
    1.19 @@ -281,11 +272,8 @@
    1.20                              else
    1.21                                raise Fail ("no type information for " ^ quote c)
    1.22                          else
    1.23 -                          if String.isPrefix skolem_theory_name c then
    1.24 -                            map fastype_of term_ts ---> HOLogic.typeT
    1.25 -                          else
    1.26 -                            Sign.const_instance thy (c,
    1.27 -                                map (type_from_fo_term tfrees) type_us))
    1.28 +                          Sign.const_instance thy (c,
    1.29 +                              map (type_from_fo_term tfrees) type_us))
    1.30            in list_comb (t, term_ts @ extra_ts) end
    1.31          | NONE => (* a free or schematic variable *)
    1.32            let
    1.33 @@ -325,12 +313,6 @@
    1.34  fun is_positive_literal (@{const Not} $ _) = false
    1.35    | is_positive_literal _ = true
    1.36  
    1.37 -(* ### FIXME: remove once Skolemization is left to ATPs *)
    1.38 -fun unskolemize_term t =
    1.39 -  Term.add_consts t []
    1.40 -  |> filter (is_skolem_const_name o fst) |> map Const
    1.41 -  |> rpair t |-> fold forall_of
    1.42 -
    1.43  val combinator_table =
    1.44    [(@{const_name COMBI}, @{thm COMBI_def_raw}),
    1.45     (@{const_name COMBK}, @{thm COMBK_def_raw}),
    1.46 @@ -445,7 +427,7 @@
    1.47      let
    1.48        val thy = ProofContext.theory_of ctxt
    1.49        val t = u |> prop_from_formula thy full_types tfrees
    1.50 -                |> unskolemize_term |> uncombine_term |> check_formula ctxt
    1.51 +                |> uncombine_term |> check_formula ctxt
    1.52      in
    1.53        (Inference (num, t, deps),
    1.54         fold Variable.declare_term (OldTerm.term_frees t) ctxt)
    1.55 @@ -626,6 +608,7 @@
    1.56    else
    1.57      apfst (insert (op =) (raw_prefix, num))
    1.58  
    1.59 +fun forall_of v t = HOLogic.all_const (fastype_of v) $ lambda v t
    1.60  fun forall_vars t = fold_rev forall_of (map Var (Term.add_vars t [])) t
    1.61  
    1.62  fun step_for_line _ _ (Definition (_, t1, t2)) = Let (t1, t2)