# HG changeset patch
# User blanchet
# Date 1319034973 -7200
# Node ID 62b8bcf2477364184932047785f0dfa48e602d4a
# Parent  154242732ef87d1f69a9bf9f3f14772181cf5de2
avoid generating too meta theorems -- this sometimes leads to type errors, e.g. when "pp" is applied to a "prop" instead of a "bool"

diff -r 154242732ef8 -r 62b8bcf24773 src/HOL/Tools/ATP/atp_translate.ML
--- a/src/HOL/Tools/ATP/atp_translate.ML	Wed Oct 19 16:32:30 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_translate.ML	Wed Oct 19 16:36:13 2011 +0200
@@ -1165,20 +1165,22 @@
       | freeze t = t
   in t |> exists_subterm is_Var t ? freeze end
 
-fun presimp_prop ctxt presimp_consts t =
-  let
-    val thy = Proof_Context.theory_of ctxt
-    val t = t |> Envir.beta_eta_contract
-              |> transform_elim_prop
-              |> Object_Logic.atomize_term thy
-    val need_trueprop = (fastype_of t = @{typ bool})
-  in
-    t |> need_trueprop ? HOLogic.mk_Trueprop
-      |> Raw_Simplifier.rewrite_term thy (Meson.unfold_set_const_simps ctxt) []
-      |> extensionalize_term ctxt
-      |> presimplify_term ctxt presimp_consts
-      |> perhaps (try (HOLogic.dest_Trueprop))
-  end
+fun presimp_prop ctxt presimp_consts role t =
+  (let
+     val thy = Proof_Context.theory_of ctxt
+     val t = t |> Envir.beta_eta_contract
+               |> transform_elim_prop
+               |> Object_Logic.atomize_term thy
+     val need_trueprop = (fastype_of t = @{typ bool})
+   in
+     t |> need_trueprop ? HOLogic.mk_Trueprop
+       |> Raw_Simplifier.rewrite_term thy (Meson.unfold_set_const_simps ctxt) []
+       |> extensionalize_term ctxt
+       |> presimplify_term ctxt presimp_consts
+       |> HOLogic.dest_Trueprop
+   end
+   handle TERM _ => if role = Conjecture then @{term False} else @{term True})
+  |> pair role
 
 (* making fact and conjecture formulas *)
 fun make_formula ctxt format type_enc eq_as_iff name loc kind t =
@@ -1199,7 +1201,8 @@
   | formula => SOME formula
 
 fun s_not_trueprop (@{const Trueprop} $ t) = @{const Trueprop} $ s_not t
-  | s_not_trueprop t = s_not t
+  | s_not_trueprop t =
+    if fastype_of t = @{typ bool} then s_not t else @{prop False} (* too meta *)
 
 fun make_conjecture ctxt format type_enc =
   map (fn ((name, loc), (kind, t)) =>
@@ -1659,7 +1662,7 @@
     val ((conjs, facts), lambdas) =
       if preproc then
         conjs @ facts
-        |> map (apsnd (apsnd (presimp_prop ctxt presimp_consts)))
+        |> map (apsnd (uncurry (presimp_prop ctxt presimp_consts)))
         |> preprocess_abstractions_in_terms trans_lambdas
         |>> chop (length conjs)
       else