src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML
changeset 41199 4698d12dd860
parent 41157 7e90d259790b
child 41211 1e2e16bc0077
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Thu Dec 16 13:54:17 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Thu Dec 16 15:12:17 2010 +0100
@@ -220,21 +220,6 @@
       | 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. *)
-val atomize_term =
-  let
-    fun aux (@{const Trueprop} $ t1) = t1
-      | aux (Const (@{const_name all}, _) $ Abs (s, T, t')) =
-        HOLogic.all_const T $ Abs (s, T, aux t')
-      | aux (@{const "==>"} $ t1 $ t2) = HOLogic.mk_imp (pairself aux (t1, t2))
-      | aux (Const (@{const_name "=="}, Type (_, [@{typ prop}, _])) $ t1 $ t2) =
-        HOLogic.eq_const HOLogic.boolT $ aux t1 $ aux t2
-      | aux (Const (@{const_name "=="}, Type (_, [T, _])) $ t1 $ t2) =
-        HOLogic.eq_const T $ t1 $ t2
-      | aux _ = raise Fail "aux"
-  in perhaps (try aux) end
-
 (* making fact and conjecture formulas *)
 fun make_formula ctxt eq_as_iff presimp name kind t =
   let