# HG changeset patch
# User blanchet
# Date 1286176126 -7200
# Node ID 97b8051033beb174a74fabc51262786e4a1b0802
# Parent  61aa00205a88012bb65e9591eb062a881a226795
renamed internal function

diff -r 61aa00205a88 -r 97b8051033be src/HOL/Tools/Sledgehammer/meson_clausify.ML
--- a/src/HOL/Tools/Sledgehammer/meson_clausify.ML	Mon Oct 04 09:05:15 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/meson_clausify.ML	Mon Oct 04 09:08:46 2010 +0200
@@ -51,9 +51,8 @@
     Const (@{const_name skolem}, T --> T) $ t
   end
 
-fun beta_eta_under_lambdas (Abs (s, T, t')) =
-    Abs (s, T, beta_eta_under_lambdas t')
-  | beta_eta_under_lambdas t = Envir.beta_eta_contract t
+fun beta_eta_in_abs_body (Abs (s, T, t')) = Abs (s, T, beta_eta_in_abs_body t')
+  | beta_eta_in_abs_body t = Envir.beta_eta_contract t
 
 (*Traverse a theorem, accumulating Skolem function definitions.*)
 fun old_skolem_defs th =
@@ -65,7 +64,7 @@
           (* Forms a lambda-abstraction over the formal parameters *)
           val rhs =
             list_abs_free (map dest_Free args,
-                           HOLogic.choice_const T $ beta_eta_under_lambdas body)
+                           HOLogic.choice_const T $ beta_eta_in_abs_body body)
             |> mk_old_skolem_term_wrapper
           val comb = list_comb (rhs, args)
         in dec_sko (subst_bound (comb, p)) (rhs :: rhss) end