1.1 --- a/src/HOL/Tools/ATP/atp_problem.ML	Mon Jun 06 20:36:34 2011 +0200
     1.2 +++ b/src/HOL/Tools/ATP/atp_problem.ML	Mon Jun 06 20:36:34 2011 +0200
     1.3 @@ -9,7 +9,7 @@
     1.4  sig
     1.5    datatype 'a fo_term = ATerm of 'a * 'a fo_term list
     1.6    datatype quantifier = AForall | AExists
     1.7 -  datatype connective = ANot | AAnd | AOr | AImplies | AIf | AIff | ANotIff
     1.8 +  datatype connective = ANot | AAnd | AOr | AImplies | AIff
     1.9    datatype ('a, 'b, 'c) formula =
    1.10      AQuant of quantifier * ('a * 'b option) list * ('a, 'b, 'c) formula |
    1.11      AConn of connective * ('a, 'b, 'c) formula list |
    1.12 @@ -93,7 +93,7 @@
    1.13  
    1.14  datatype 'a fo_term = ATerm of 'a * 'a fo_term list
    1.15  datatype quantifier = AForall | AExists
    1.16 -datatype connective = ANot | AAnd | AOr | AImplies | AIf | AIff | ANotIff
    1.17 +datatype connective = ANot | AAnd | AOr | AImplies | AIff
    1.18  datatype ('a, 'b, 'c) formula =
    1.19    AQuant of quantifier * ('a * 'b option) list * ('a, 'b, 'c) formula |
    1.20    AConn of connective * ('a, 'b, 'c) formula list |
    1.21 @@ -147,9 +147,7 @@
    1.22    | raw_polarities_of_conn AAnd = (SOME true, SOME true)
    1.23    | raw_polarities_of_conn AOr = (SOME true, SOME true)
    1.24    | raw_polarities_of_conn AImplies = (SOME false, SOME true)
    1.25 -  | raw_polarities_of_conn AIf = (SOME true, SOME false)
    1.26    | raw_polarities_of_conn AIff = (NONE, NONE)
    1.27 -  | raw_polarities_of_conn ANotIff = (NONE, NONE)
    1.28  fun polarities_of_conn NONE = K (NONE, NONE)
    1.29    | polarities_of_conn (SOME pos) =
    1.30      raw_polarities_of_conn #> not pos ? pairself (Option.map not)
    1.31 @@ -235,9 +233,7 @@
    1.32    | string_for_connective AAnd = tptp_and
    1.33    | string_for_connective AOr = tptp_or
    1.34    | string_for_connective AImplies = tptp_implies
    1.35 -  | string_for_connective AIf = tptp_if
    1.36    | string_for_connective AIff = tptp_iff
    1.37 -  | string_for_connective ANotIff = tptp_not_iff
    1.38  
    1.39  fun string_for_bound_var format (s, ty) =
    1.40    s ^ (if format = TFF orelse format = THF then
    1.41 @@ -341,14 +337,10 @@
    1.42      AConn (AOr, map (clausify_formula1 true) phis)
    1.43    | clausify_formula1 true (AConn (AImplies, [phi1, phi2])) =
    1.44      AConn (AOr, [clausify_formula1 false phi1, clausify_formula1 true phi2])
    1.45 -  | clausify_formula1 true (AConn (AIf, phis)) =
    1.46 -    clausify_formula1 true (AConn (AImplies, rev phis))
    1.47    | clausify_formula1 _ _ = raise CLAUSIFY ()
    1.48  fun clausify_formula true (AConn (AIff, phis)) =
    1.49 -    [clausify_formula1 true (AConn (AIf, phis)),
    1.50 +    [clausify_formula1 true (AConn (AImplies, rev phis)),
    1.51       clausify_formula1 true (AConn (AImplies, phis))]
    1.52 -  | clausify_formula false (AConn (ANotIff, phis)) =
    1.53 -    clausify_formula true (AConn (AIff, phis))
    1.54    | clausify_formula pos phi = [clausify_formula1 pos phi]
    1.55  
    1.56  fun clausify_formula_line (Formula (ident, kind, phi, source, info)) =