# HG changeset patch
# User blanchet
# Date 1282219314 -7200
# Node ID cda5f200042766e789ac4e4e9233fd43a45a80df
# Parent  a57d04dd1b256bd96dfe98c6a65538480c6aa554
improve atomization

diff -r a57d04dd1b25 -r cda5f2000427 src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML	Thu Aug 19 13:04:37 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML	Thu Aug 19 14:01:54 2010 +0200
@@ -151,12 +151,27 @@
       | aux t = t
   in t |> exists_subterm is_Var t ? aux end
 
+(* "Object_Logic.atomize_term" isn't as powerful as it could be; for example,
+    it leaves metaequalities over "prop"s alone. *)
+fun atomize_term t =
+  (case t of
+     @{const Trueprop} $ t1 => t1
+   | Const (@{const_name all}, _) $ Abs (s, T, t') =>
+     HOLogic.all_const T $ Abs (s, T, atomize_term t')
+   | @{const "==>"} $ t1 $ t2 => HOLogic.mk_imp (pairself atomize_term (t1, t2))
+   | Const (@{const_name "=="}, Type (_, [@{typ prop}, _])) $ t1 $ t2 =>
+     HOLogic.eq_const HOLogic.boolT $ atomize_term t1 $ atomize_term t2
+   | Const (@{const_name "=="}, Type (_, [T, _])) $ t1 $ t2 =>
+     HOLogic.eq_const T $ t1 $ t2
+   | _ => raise Fail "atomize_term")
+  handle Fail "atomize_term" => t
+
 (* making axiom and conjecture formulas *)
 fun make_formula ctxt presimp (name, kind, t) =
   let
     val thy = ProofContext.theory_of ctxt
     val t = t |> transform_elim_term
-              |> Object_Logic.atomize_term thy
+              |> atomize_term
     val t = t |> fastype_of t = HOLogic.boolT ? HOLogic.mk_Trueprop
               |> extensionalize_term
               |> presimp ? presimplify_term thy