# HG changeset patch
# User blanchet
# Date 1280157759 -7200
# Node ID f1b7fb87f5231350b89c575d6bd42e275c7c504a
# Parent  abf8a79853c93b1881127bdbb10323c9f7d13e91
remove more Skolemization-aware code

diff -r abf8a79853c9 -r f1b7fb87f523 src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML
--- 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)