--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Mon Jul 26 17:17:59 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Mon Jul 26 17:22:39 2010 +0200
@@ -43,15 +43,6 @@
fun is_conjecture_clause_number conjecture_shape num =
index_in_shape num conjecture_shape >= 0
-fun smart_lambda v t =
- Abs (case v of
- Const (s, _) =>
- List.last (space_explode skolem_infix (Long_Name.base_name s))
- | Var ((s, _), _) => s
- | Free (s, _) => s
- | _ => "", fastype_of v, abstract_over (v, t))
-fun forall_of v t = HOLogic.all_const (fastype_of v) $ smart_lambda v t
-
fun negate_term (Const (@{const_name All}, T) $ Abs (s, T', t')) =
Const (@{const_name Ex}, T) $ Abs (s, T', negate_term t')
| negate_term (Const (@{const_name Ex}, T) $ Abs (s, T', t')) =
@@ -281,11 +272,8 @@
else
raise Fail ("no type information for " ^ quote c)
else
- if String.isPrefix skolem_theory_name c then
- map fastype_of term_ts ---> HOLogic.typeT
- else
- Sign.const_instance thy (c,
- map (type_from_fo_term tfrees) type_us))
+ Sign.const_instance thy (c,
+ map (type_from_fo_term tfrees) type_us))
in list_comb (t, term_ts @ extra_ts) end
| NONE => (* a free or schematic variable *)
let
@@ -325,12 +313,6 @@
fun is_positive_literal (@{const Not} $ _) = false
| is_positive_literal _ = true
-(* ### FIXME: remove once Skolemization is left to ATPs *)
-fun unskolemize_term t =
- Term.add_consts t []
- |> filter (is_skolem_const_name o fst) |> map Const
- |> rpair t |-> fold forall_of
-
val combinator_table =
[(@{const_name COMBI}, @{thm COMBI_def_raw}),
(@{const_name COMBK}, @{thm COMBK_def_raw}),
@@ -445,7 +427,7 @@
let
val thy = ProofContext.theory_of ctxt
val t = u |> prop_from_formula thy full_types tfrees
- |> unskolemize_term |> uncombine_term |> check_formula ctxt
+ |> uncombine_term |> check_formula ctxt
in
(Inference (num, t, deps),
fold Variable.declare_term (OldTerm.term_frees t) ctxt)
@@ -626,6 +608,7 @@
else
apfst (insert (op =) (raw_prefix, num))
+fun forall_of v t = HOLogic.all_const (fastype_of v) $ lambda v t
fun forall_vars t = fold_rev forall_of (map Var (Term.add_vars t [])) t
fun step_for_line _ _ (Definition (_, t1, t2)) = Let (t1, t2)