# HG changeset patch
# User blanchet
# Date 1351679001 -3600
# Node ID 724cfe0131823845c03cb6874c8c25140d75cb61
# Parent  e12b4e9794fdb4633f633a0bf77e851e14ac6a10
tuned code

diff -r e12b4e9794fd -r 724cfe013182 src/HOL/Tools/ATP/atp_problem_generate.ML
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Wed Oct 31 11:23:21 2012 +0100
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Wed Oct 31 11:23:21 2012 +0100
@@ -788,7 +788,7 @@
   | constify_lifted t = t
 
 fun lift_lams_part_1 ctxt type_enc =
-  map close_form #> rpair ctxt
+  map hol_close_form #> rpair ctxt
   #-> Lambda_Lifting.lift_lambdas
           (SOME ((if is_type_enc_polymorphic type_enc then
                     lam_lifted_poly_prefix
@@ -805,8 +805,8 @@
   |> pairself (map constify_lifted)
   (* Requires bound variables not to clash with any schematic variables (as
      should be the case right after lambda-lifting). *)
-  |>> map (open_form (unprefix close_form_prefix))
-  ||> map (open_form I)
+  |>> map (hol_open_form (unprefix hol_close_form_prefix))
+  ||> map (hol_open_form I)
 
 fun lift_lams ctxt = lift_lams_part_2 ctxt oo lift_lams_part_1 ctxt
 
diff -r e12b4e9794fd -r 724cfe013182 src/HOL/Tools/ATP/atp_util.ML
--- a/src/HOL/Tools/ATP/atp_util.ML	Wed Oct 31 11:23:21 2012 +0100
+++ b/src/HOL/Tools/ATP/atp_util.ML	Wed Oct 31 11:23:21 2012 +0100
@@ -34,9 +34,9 @@
   val s_disj : term * term -> term
   val s_imp : term * term -> term
   val s_iff : term * term -> term
-  val close_form_prefix : string
-  val close_form : term -> term
-  val open_form : (string -> string) -> term -> term
+  val hol_close_form_prefix : string
+  val hol_close_form : term -> term
+  val hol_open_form : (string -> string) -> term -> term
   val monomorphic_term : Type.tyenv -> term -> term
   val eta_expand : typ list -> term -> int -> term
   val cong_extensionalize_term : theory -> term -> term
@@ -298,24 +298,25 @@
   | s_iff (t1, @{const True}) = t1
   | s_iff (t1, t2) = HOLogic.eq_const HOLogic.boolT $ t1 $ t2
 
-val close_form_prefix = "ATP.close_form."
+val hol_close_form_prefix = "ATP.close_form."
 
-fun close_form t =
+fun hol_close_form t =
   fold (fn ((s, i), T) => fn t' =>
            HOLogic.all_const T
-           $ Abs (close_form_prefix ^ s, T,
+           $ Abs (hol_close_form_prefix ^ s, T,
                   abstract_over (Var ((s, i), T), t')))
        (Term.add_vars t []) t
 
-fun open_form unprefix (t as Const (@{const_name All}, _) $ Abs (s, T, t')) =
+fun hol_open_form unprefix
+      (t as Const (@{const_name All}, _) $ Abs (s, T, t')) =
     (case try unprefix s of
        SOME s =>
        let
          val names = Name.make_context (map fst (Term.add_var_names t' []))
          val (s, _) = Name.variant s names
-       in open_form unprefix (subst_bound (Var ((s, 0), T), t')) end
+       in hol_open_form unprefix (subst_bound (Var ((s, 0), T), t')) end
      | NONE => t)
-  | open_form _ t = t
+  | hol_open_form _ t = t
 
 fun monomorphic_term subst =
   map_types (map_type_tvar (fn v =>