prevent schematic variable clash in combinator-introduction code, when invoked from Sledgehammer (another consequence of the CNF -> FOF transition)

--- a/src/HOL/Tools/ATP_Manager/atp_systems.ML	Mon Jul 26 22:35:25 2010 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_systems.ML	Mon Jul 26 23:54:40 2010 +0200
@@ -187,8 +187,9 @@
   subst_atomic (map (fn (j, T) => (Free (concealed_bound_name j, T), Bound j))
                     (0 upto length Ts - 1 ~~ Ts))
 
-fun introduce_combinators_in_term thy t =
+fun introduce_combinators_in_term ctxt kind t =
   let
+    val thy = ProofContext.theory_of ctxt
     fun aux Ts t =
       case t of
         @{const Not} $ t1 => @{const Not} $ aux Ts t1
@@ -205,37 +206,44 @@
       | _ => if not (exists_subterm (fn Abs _ => true | _ => false) t) then
                t
              else
-               t |> conceal_bounds Ts
-                 |> Envir.eta_contract
-                 |> cterm_of thy
-                 |> Clausifier.introduce_combinators_in_cterm
-                 |> prop_of |> Logic.dest_equals |> snd
-                 |> reveal_bounds Ts
-               handle THM (msg, _, _) =>
-                      (* A type variable of sort "{}" will make abstraction
-                         fail. *)
-                      t
+               let
+                 val t = t |> conceal_bounds Ts
+                           |> Envir.eta_contract
+                 val ([t], ctxt') = Variable.import_terms true [t] ctxt
+               in
+                 t |> cterm_of thy
+                   |> Clausifier.introduce_combinators_in_cterm
+                   |> singleton (Variable.export ctxt' ctxt)
+                   |> prop_of |> Logic.dest_equals |> snd
+                   |> reveal_bounds Ts
+               end
   in t |> not (Meson.is_fol_term thy t) ? aux [] end
+  handle THM _ =>
+         (* A type variable of sort "{}" will make abstraction fail. *)
+         case kind of
+           Axiom => HOLogic.true_const
+         | Conjecture => HOLogic.false_const
 
 (* making axiom and conjecture clauses *)
-fun make_clause thy (formula_name, kind, t) =
+fun make_clause ctxt (formula_name, kind, t) =
   let
+    val thy = ProofContext.theory_of ctxt
     (* ### FIXME: perform other transformations previously done by
        "Clausifier.to_nnf", e.g. "HOL.If" *)
     val t = t |> transform_elim_term
               |> Object_Logic.atomize_term thy
               |> extensionalize_term
-              |> introduce_combinators_in_term thy
+              |> introduce_combinators_in_term ctxt kind
     val (combformula, ctypes_sorts) = combformula_for_prop thy t []
   in
     FOLFormula {formula_name = formula_name, combformula = combformula,
                 kind = kind, ctypes_sorts = ctypes_sorts}
   end
 
-fun make_axiom_clause thy (name, th) =
-  (name, make_clause thy (name, Axiom, prop_of th))
-fun make_conjecture_clauses thy ts =
-  map2 (fn j => fn t => make_clause thy (Int.toString j, Conjecture, t))
+fun make_axiom_clause ctxt (name, th) =
+  (name, make_clause ctxt (name, Axiom, prop_of th))
+fun make_conjecture_clauses ctxt ts =
+  map2 (fn j => fn t => make_clause ctxt (Int.toString j, Conjecture, t))
        (0 upto length ts - 1) ts
 
 (** Helper clauses **)
@@ -263,7 +271,7 @@
   Symtab.make (maps (maps (map (rpair 0) o fst))
                     [optional_helpers, optional_typed_helpers])
 
-fun get_helper_clauses thy is_FO full_types conjectures axclauses =
+fun get_helper_clauses ctxt is_FO full_types conjectures axclauses =
   let
     val ct = fold (fold count_fol_formula) [conjectures, axclauses]
                   init_counters
@@ -275,31 +283,35 @@
                    if exists is_needed ss then map (`Thm.get_name_hint) ths
                    else [])) @
       (if is_FO then [] else map (`Thm.get_name_hint) mandatory_helpers)
-  in map (snd o make_axiom_clause thy) cnfs end
+  in map (snd o make_axiom_clause ctxt) cnfs end
 
 fun s_not (@{const Not} $ t) = t
   | s_not t = @{const Not} $ t
 
 (* prepare for passing to writer,
    create additional clauses based on the information from extra_cls *)
-fun prepare_clauses full_types hyp_ts concl_t axcls extra_cls thy =
+fun prepare_clauses ctxt full_types hyp_ts concl_t axcls extra_cls =
   let
+    val thy = ProofContext.theory_of ctxt
     val goal_t = Logic.list_implies (hyp_ts, concl_t)
     val is_FO = Meson.is_fol_term thy goal_t
-    val _ = trace_msg (fn _ => Syntax.string_of_term_global thy goal_t)
+    val _ = trace_msg (fn _ => Syntax.string_of_term ctxt goal_t)
     val axtms = map (prop_of o snd) extra_cls
     val subs = tfree_classes_of_terms [goal_t]
     val supers = tvar_classes_of_terms axtms
     val tycons = type_consts_of_terms thy (goal_t :: axtms)
     (* TFrees in conjecture clauses; TVars in axiom clauses *)
-    val conjectures = make_conjecture_clauses thy (map s_not hyp_ts @ [concl_t])
-    val extra_clauses = map (snd o make_axiom_clause thy) extra_cls
+    val conjectures =
+      map (s_not o HOLogic.dest_Trueprop) hyp_ts @
+        [HOLogic.dest_Trueprop concl_t]
+      |> make_conjecture_clauses ctxt
+    val extra_clauses = map (snd o make_axiom_clause ctxt) extra_cls
     val (clnames, axiom_clauses) =
-      ListPair.unzip (map (make_axiom_clause thy) axcls)
+      ListPair.unzip (map (make_axiom_clause ctxt) axcls)
     (* FIXME: Should it read "extra_clauses" or "axiom_clauses" in the
        "get_helper_clauses" call? *)
     val helper_clauses =
-      get_helper_clauses thy is_FO full_types conjectures extra_clauses
+      get_helper_clauses ctxt is_FO full_types conjectures extra_clauses
     val (supers', arity_clauses) = make_arity_clauses thy tycons supers
     val class_rel_clauses = make_class_rel_clauses thy subs supers'
   in
@@ -367,7 +379,7 @@
   let
     (* get clauses and prepare them for writing *)
     val (ctxt, (_, th)) = goal;
-    val thy = ProofContext.theory_of ctxt;
+    val thy = ProofContext.theory_of ctxt
     (* ### FIXME: (1) preprocessing for "if" etc. *)
     val (params, hyp_ts, concl_t) = strip_subgoal th subgoal
     val the_filtered_clauses =
@@ -379,8 +391,8 @@
                     relevance_override goal hyp_ts concl_t
     val the_axiom_clauses = axiom_clauses |> the_default the_filtered_clauses
     val (internal_thm_names, clauses) =
-      prepare_clauses full_types hyp_ts concl_t the_axiom_clauses
-                      the_filtered_clauses thy
+      prepare_clauses ctxt full_types hyp_ts concl_t the_axiom_clauses
+                      the_filtered_clauses
 
     (* path to unique problem file *)
     val the_dest_dir = if overlord then getenv "ISABELLE_HOME_USER"

--- a/src/HOL/Tools/Sledgehammer/clausifier.ML	Mon Jul 26 22:35:25 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/clausifier.ML	Mon Jul 26 23:54:40 2010 +0200
@@ -109,8 +109,11 @@
       val thy = theory_of_cterm ct
       val Abs(x,_,body) = term_of ct
       val Type(@{type_name fun}, [xT,bodyT]) = typ_of (ctyp_of_term ct)
-      val cxT = ctyp_of thy xT and cbodyT = ctyp_of thy bodyT
-      fun makeK() = instantiate' [SOME cxT, SOME cbodyT] [SOME (cterm_of thy body)] @{thm abs_K}
+      val cxT = ctyp_of thy xT
+      val cbodyT = ctyp_of thy bodyT
+      fun makeK () =
+        instantiate' [SOME cxT, SOME cbodyT] [SOME (cterm_of thy body)]
+                     @{thm abs_K}
   in
       case body of
           Const _ => makeK()

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_tptp_format.ML	Mon Jul 26 22:35:25 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_tptp_format.ML	Mon Jul 26 23:54:40 2010 +0200
@@ -77,6 +77,8 @@
 fun string_for_formula (AQuant (q, xs, phi)) =
     string_for_quantifier q ^ "[" ^ commas xs ^ "]: " ^
     string_for_formula phi
+  | string_for_formula (AConn (ANot, [APred (ATerm ("equal", ts))])) =
+    space_implode " != " (map string_for_term ts)
   | string_for_formula (AConn (c, [phi])) =
     string_for_connective c ^ " " ^ string_for_formula phi
   | string_for_formula (AConn (c, phis)) =