--- a/src/HOL/Tools/ATP/atp_problem.ML Sun May 01 18:37:24 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_problem.ML Sun May 01 18:37:24 2011 +0200
@@ -11,7 +11,7 @@
datatype quantifier = AForall | AExists
datatype connective = ANot | AAnd | AOr | AImplies | AIf | AIff | ANotIff
datatype ('a, 'b) formula =
- AQuant of quantifier * 'a list * ('a, 'b) formula |
+ AQuant of quantifier * ('a * 'a option) list * ('a, 'b) formula |
AConn of connective * ('a, 'b) formula list |
AAtom of 'b
type 'a uniform_formula = ('a, 'a fo_term) formula
@@ -42,7 +42,7 @@
datatype quantifier = AForall | AExists
datatype connective = ANot | AAnd | AOr | AImplies | AIf | AIff | ANotIff
datatype ('a, 'b) formula =
- AQuant of quantifier * 'a list * ('a, 'b) formula |
+ AQuant of quantifier * ('a * 'a option) list * ('a, 'b) formula |
AConn of connective * ('a, 'b) formula list |
AAtom of 'b
type 'a uniform_formula = ('a, 'a fo_term) formula
@@ -79,8 +79,11 @@
| string_for_connective AIf = "<="
| string_for_connective AIff = "<=>"
| string_for_connective ANotIff = "<~>"
+fun string_for_bound_var (s, NONE) = s
+ | string_for_bound_var (s, SOME t) = s ^ " : " ^ t
fun string_for_formula (AQuant (q, xs, phi)) =
- "(" ^ string_for_quantifier q ^ "[" ^ commas xs ^ "] : " ^
+ "(" ^ string_for_quantifier q ^
+ "[" ^ commas (map string_for_bound_var xs) ^ "] : " ^
string_for_formula phi ^ ")"
| string_for_formula (AConn (ANot, [AAtom (ATerm ("equal", ts))])) =
space_implode " != " (map string_for_term ts)
@@ -179,8 +182,11 @@
fun nice_term (ATerm (name, ts)) =
nice_name name ##>> pool_map nice_term ts #>> ATerm
fun nice_formula (AQuant (q, xs, phi)) =
- pool_map nice_name xs ##>> nice_formula phi
- #>> (fn (xs, phi) => AQuant (q, xs, phi))
+ pool_map nice_name (map fst xs)
+ ##>> pool_map (fn NONE => pair NONE
+ | SOME s => nice_name s #>> SOME) (map snd xs)
+ ##>> nice_formula phi
+ #>> (fn ((ss, ts), phi) => AQuant (q, ss ~~ ts, phi))
| nice_formula (AConn (c, phis)) =
pool_map nice_formula phis #>> curry AConn c
| nice_formula (AAtom tm) = nice_term tm #>> AAtom