# HG changeset patch
# User blanchet
# Date 1387210732 -3600
# Node ID ee0881a54c72d96ce1681e65391fdc0399c2bd23
# Parent  81290fe85890e562e6488ccf1bc1909d54d159fc
fixed confusion between 'prop' and 'bool' introduced in 4960647932ec

diff -r 81290fe85890 -r ee0881a54c72 src/HOL/Tools/ATP/atp_problem_generate.ML
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Mon Dec 16 14:49:18 2013 +0100
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Mon Dec 16 17:18:52 2013 +0100
@@ -1958,6 +1958,10 @@
         end
   in List.partition (curry (op =) Definition o #role) #>> reorder [] #> op @ end
 
+fun s_not_prop (@{const Trueprop} $ t) = @{const Trueprop} $ s_not t
+  | s_not_prop (@{const "==>"} $ t $ @{prop False}) = t
+  | s_not_prop t = @{const "==>"} $ t $ @{prop False}
+
 fun translate_formulas ctxt prem_role format type_enc lam_trans presimp hyp_ts
                        concl_t facts =
   let
diff -r 81290fe85890 -r ee0881a54c72 src/HOL/Tools/ATP/atp_proof_reconstruct.ML
--- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Mon Dec 16 14:49:18 2013 +0100
+++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Mon Dec 16 17:18:52 2013 +0100
@@ -334,9 +334,8 @@
       | AQuant (q, (s, _) :: xs, phi') =>
         do_formula pos (AQuant (q, xs, phi'))
         (* FIXME: TFF *)
-        #>> quantify_over_var
-              (case q of AForall => forall_of | AExists => exists_of)
-              (s |> textual ? repair_var_name)
+        #>> quantify_over_var (case q of AForall => forall_of | AExists => exists_of)
+          (s |> textual ? repair_var_name)
       | AConn (ANot, [phi']) => do_formula (not pos) phi' #>> s_not
       | AConn (c, [phi1, phi2]) =>
         do_formula (pos |> c = AImplies ? not) phi1
diff -r 81290fe85890 -r ee0881a54c72 src/HOL/Tools/ATP/atp_util.ML
--- a/src/HOL/Tools/ATP/atp_util.ML	Mon Dec 16 14:49:18 2013 +0100
+++ b/src/HOL/Tools/ATP/atp_util.ML	Mon Dec 16 17:18:52 2013 +0100
@@ -36,7 +36,6 @@
   val s_disj : term * term -> term
   val s_imp : term * term -> term
   val s_iff : term * term -> term
-  val s_not_prop : term -> term
   val close_form : term -> term
   val hol_close_form_prefix : string
   val hol_close_form : term -> term
@@ -308,10 +307,6 @@
   | s_iff (t1, @{const False}) = s_not t1
   | s_iff (t1, t2) = HOLogic.eq_const HOLogic.boolT $ t1 $ t2
 
-fun s_not_prop (@{const Trueprop} $ t) = @{const Trueprop} $ s_not t
-  | s_not_prop (@{const "==>"} $ t $ @{prop False}) = t
-  | s_not_prop t = @{const "==>"} $ t $ @{prop False}
-
 fun close_form t =
   fold (fn ((s, i), T) => fn t' =>
       Logic.all_const T $ Abs (s, T, abstract_over (Var ((s, i), T), t')))
diff -r 81290fe85890 -r ee0881a54c72 src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Mon Dec 16 14:49:18 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Mon Dec 16 17:18:52 2013 +0100
@@ -324,8 +324,10 @@
           |> fold (fn (name as (s, _), role, t, rule, _) =>
               Symtab.update_new (s, (rule, t
                 |> (if is_clause_tainted [name] then
-                      role <> Conjecture ? s_not_prop
+                      HOLogic.dest_Trueprop
+                      #> role <> Conjecture ? s_not
                       #> fold exists_of (map Var (Term.add_vars t []))
+                      #> HOLogic.mk_Trueprop
                     else
                       I))))
             atp_proof