src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML
changeset 42943 62a14c80d194
parent 42939 0134d6650092
child 42944 9e620869a576
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Sun May 22 14:51:04 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Sun May 22 14:51:41 2011 +0200
@@ -247,8 +247,6 @@
        |> filter (fn TyLitVar _ => kind <> Conjecture
                    | TyLitFree _ => kind = Conjecture)
 
-fun mk_anot phi = AConn (ANot, [phi])
-fun mk_aconn c phi1 phi2 = AConn (c, [phi1, phi2])
 fun mk_aconns c phis =
   let val (phis', phi') = split_last phis in
     fold_rev (mk_aconn c) phis' phi'