# HG changeset patch
# User blanchet
# Date 1304267844 -7200
# Node ID f64c546efe8c70b1cb4b92b53b9add721c574976
# Parent  747736d8b47e26010366b88899beceefc1c79f6b
fixed type of ATP quantifier types (sic)

diff -r 747736d8b47e -r f64c546efe8c src/HOL/Tools/ATP/atp_problem.ML
--- 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 * 'a option) list * ('a, 'b) formula |
+    AQuant of quantifier * ('a * 'b 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 * 'a option) list * ('a, 'b) formula |
+  AQuant of quantifier * ('a * 'b option) list * ('a, 'b) formula |
   AConn of connective * ('a, 'b) formula list |
   AAtom of 'b
 type 'a uniform_formula = ('a, 'a fo_term) formula
@@ -80,7 +80,7 @@
   | 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
+  | string_for_bound_var (s, SOME ty) = s ^ " : " ^ string_for_term ty
 fun string_for_formula (AQuant (q, xs, phi)) =
     "(" ^ string_for_quantifier q ^
     "[" ^ commas (map string_for_bound_var xs) ^ "] : " ^
@@ -201,7 +201,7 @@
 fun nice_formula (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)
+                    | SOME ty => nice_term ty #>> SOME) (map snd xs)
     ##>> nice_formula phi
     #>> (fn ((ss, ts), phi) => AQuant (q, ss ~~ ts, phi))
   | nice_formula (AConn (c, phis)) =
diff -r 747736d8b47e -r f64c546efe8c src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Sun May 01 18:37:24 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Sun May 01 18:37:24 2011 +0200
@@ -447,9 +447,9 @@
     (hd ss, map unmangled_type (tl ss))
   end
 
-fun fo_term_for_combterm ctxt type_sys =
+fun formula_for_combformula ctxt type_sys =
   let
-    fun aux top_level u =
+    fun do_term top_level u =
       let
         val (head, args) = strip_combterm_comb u
         val (x, ty_args) =
@@ -478,23 +478,20 @@
                  end)
           | CombVar (name, _) => (name, [])
           | CombApp _ => raise Fail "impossible \"CombApp\""
-        val t =
-          ATerm (x, map fo_term_for_combtyp ty_args @ map (aux false) args)
+        val t = ATerm (x, map fo_term_for_combtyp ty_args @
+                          map (do_term false) args)
         val ty = combtyp_of u
-    in
-      t |> (if should_tag_with_type ctxt type_sys ty then
-              tag_with_type (fo_term_for_combtyp ty)
-            else
-              I)
-    end
-  in aux true end
-
-fun formula_for_combformula ctxt type_sys =
-  let
-    fun aux (AQuant (q, xs, phi)) = AQuant (q, xs, aux phi)
-      | aux (AConn (c, phis)) = AConn (c, map aux phis)
-      | aux (AAtom tm) = AAtom (fo_term_for_combterm ctxt type_sys tm)
-  in aux end
+      in
+        t |> (if should_tag_with_type ctxt type_sys ty then
+                tag_with_type (fo_term_for_combtyp ty)
+              else
+                I)
+      end
+    fun do_formula (AQuant (q, xs, phi)) =
+        AQuant (q, map (apsnd (Option.map (do_term true))) xs, do_formula phi)
+      | do_formula (AConn (c, phis)) = AConn (c, map do_formula phis)
+      | do_formula (AAtom tm) = AAtom (do_term true tm)
+  in do_formula end
 
 fun formula_for_fact ctxt type_sys
                      ({combformula, ctypes_sorts, ...} : translated_formula) =