# HG changeset patch
# User blanchet
# Date 1284448348 -7200
# Node ID 104a6d9e493edb1c4bb1ec480a2a524b21e8e19c
# Parent  cd20519eb9d027267f9afac2c2e38978d4e415cd
rename internal Sledgehammer constant

diff -r cd20519eb9d0 -r 104a6d9e493e src/HOL/Sledgehammer.thy
--- a/src/HOL/Sledgehammer.thy	Tue Sep 14 08:50:46 2010 +0200
+++ b/src/HOL/Sledgehammer.thy	Tue Sep 14 09:12:28 2010 +0200
@@ -29,8 +29,8 @@
 lemma TruepropI: "P \<equiv> Q \<Longrightarrow> Trueprop P \<equiv> Trueprop Q"
 by simp
 
-definition skolem_id :: "'a \<Rightarrow> 'a" where
-[no_atp]: "skolem_id = (\<lambda>x. x)"
+definition skolem :: "'a \<Rightarrow> 'a" where
+[no_atp]: "skolem = (\<lambda>x. x)"
 
 definition COMBI :: "'a \<Rightarrow> 'a" where
 [no_atp]: "COMBI P = P"
diff -r cd20519eb9d0 -r 104a6d9e493e src/HOL/Tools/Sledgehammer/clausifier.ML
--- a/src/HOL/Tools/Sledgehammer/clausifier.ML	Tue Sep 14 08:50:46 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/clausifier.ML	Tue Sep 14 09:12:28 2010 +0200
@@ -40,9 +40,9 @@
 
 (**** SKOLEMIZATION BY INFERENCE (lcp) ****)
 
-fun mk_skolem_id t =
+fun mk_skolem t =
   let val T = fastype_of t in
-    Const (@{const_name skolem_id}, T --> T) $ t
+    Const (@{const_name skolem}, T --> T) $ t
   end
 
 fun beta_eta_under_lambdas (Abs (s, T, t')) =
@@ -62,7 +62,7 @@
           val rhs =
             list_abs_free (map dest_Free args,
                            HOLogic.choice_const T $ beta_eta_under_lambdas body)
-            |> mk_skolem_id
+            |> mk_skolem
           val comb = list_comb (rhs, args)
         in dec_sko (subst_bound (comb, p)) (rhs :: rhss) end
       | dec_sko (Const (@{const_name All},_) $ Abs (a, T, p)) rhss =
@@ -88,7 +88,7 @@
          $ _ $ Abs (s, _, _)) => extensionalize_theorem (th RS fun_cong_all)
   | _ => th
 
-fun is_quasi_lambda_free (Const (@{const_name skolem_id}, _) $ _) = true
+fun is_quasi_lambda_free (Const (@{const_name skolem}, _) $ _) = true
   | is_quasi_lambda_free (t1 $ t2) =
     is_quasi_lambda_free t1 andalso is_quasi_lambda_free t2
   | is_quasi_lambda_free (Abs _) = false
@@ -188,7 +188,7 @@
       in  c_variant_abs_multi (ct, cv::vars)  end
       handle CTERM _ => (ct0, rev vars);
 
-val skolem_id_def_raw = @{thms skolem_id_def_raw}
+val skolem_def_raw = @{thms skolem_def_raw}
 
 (* Given the definition of a Skolem function, return a theorem to replace
    an existential formula by a use of that function.
@@ -209,8 +209,8 @@
       Drule.list_comb (rhs, frees)
       |> Drule.beta_conv cabs |> Thm.capply cTrueprop
     fun tacf [prem] =
-      rewrite_goals_tac skolem_id_def_raw
-      THEN rtac ((prem |> rewrite_rule skolem_id_def_raw) RS @{thm someI_ex}) 1
+      rewrite_goals_tac skolem_def_raw
+      THEN rtac ((prem |> rewrite_rule skolem_def_raw) RS @{thm someI_ex}) 1
   in
     Goal.prove_internal [ex_tm] conc tacf
     |> forall_intr_list frees
diff -r cd20519eb9d0 -r 104a6d9e493e src/HOL/Tools/Sledgehammer/metis_clauses.ML
--- a/src/HOL/Tools/Sledgehammer/metis_clauses.ML	Tue Sep 14 08:50:46 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/metis_clauses.ML	Tue Sep 14 09:12:28 2010 +0200
@@ -443,10 +443,10 @@
   skolem_infix ^ "g"
 
 fun conceal_skolem_terms i skolems t =
-  if exists_Const (curry (op =) @{const_name skolem_id} o fst) t then
+  if exists_Const (curry (op =) @{const_name skolem} o fst) t then
     let
       fun aux skolems
-              (t as (Const (@{const_name skolem_id}, Type (_, [_, T])) $ _)) =
+              (t as (Const (@{const_name skolem}, Type (_, [_, T])) $ _)) =
           let
             val (skolems, s) =
               if i = ~1 then
@@ -513,7 +513,7 @@
     fun aux (Const x) =
         fold (fold_type_consts set_insert) (Sign.const_typargs thy x)
       | aux (Abs (_, _, u)) = aux u
-      | aux (Const (@{const_name skolem_id}, _) $ _) = I
+      | aux (Const (@{const_name skolem}, _) $ _) = I
       | aux (t $ u) = aux t #> aux u
       | aux _ = I
   in aux end