diff -r 1016664b8feb -r 9aa0fad4e864 src/HOL/Tools/ATP/atp_proof.ML
--- a/src/HOL/Tools/ATP/atp_proof.ML	Tue Jun 26 11:14:39 2012 +0200
+++ b/src/HOL/Tools/ATP/atp_proof.ML	Tue Jun 26 11:14:39 2012 +0200
@@ -54,7 +54,8 @@
   val scan_general_id : string list -> string * string list
   val satallax_unsat_coreN : string
   val parse_formula :
-    string list -> (string, 'a, (string, 'a) ho_term) formula * string list
+    string list
+    -> (string, 'a, (string, 'a) ho_term) formula * string list
   val atp_proof_from_tstplike_proof : string problem -> string -> string proof
   val clean_up_atp_proof_dependencies : string proof -> string proof
   val map_term_names_in_atp_proof :
@@ -251,7 +252,7 @@
   File_Source of string * string option |
   Inference_Source of string * string list
 
-val dummy_phi = AAtom (ATerm ("", []))
+val dummy_phi = AAtom (ATerm (("", []), []))
 val dummy_inference = Inference_Source ("", [])
 
 (* "skip_term" is there to cope with Waldmeister nonsense such as
@@ -271,7 +272,7 @@
    || skip_term >> K dummy_inference) x
 
 fun list_app (f, args) =
-  fold (fn arg => fn f => ATerm (tptp_app, [f, arg])) args f
+  fold (fn arg => fn f => ATerm ((tptp_app, []), [f, arg])) args f
 
 (* We currently ignore TFF and THF types. *)
 fun parse_type_stuff x =
@@ -280,7 +281,7 @@
   ($$ "(" |-- parse_term --| $$ ")" --| parse_type_stuff
    || scan_general_id --| parse_type_stuff
         -- Scan.optional ($$ "(" |-- parse_terms --| $$ ")") []
-      >> ATerm) x
+      >> (ATerm o apfst (rpair []))) x
 and parse_term x =
   (parse_arg -- Scan.repeat ($$ tptp_app |-- parse_arg) >> list_app) x
 and parse_terms x =
@@ -291,7 +292,7 @@
                               -- parse_term)
    >> (fn (u1, NONE) => AAtom u1
         | (u1, SOME (neg, u2)) =>
-          AAtom (ATerm ("equal", [u1, u2])) |> is_some neg ? mk_anot)) x
+          AAtom (ATerm (("equal", []), [u1, u2])) |> is_some neg ? mk_anot)) x
 
 (* TPTP formulas are fully parenthesized, so we don't need to worry about
    operator precedence. *)
@@ -323,7 +324,7 @@
    --| $$ "[" -- parse_terms --| $$ "]" --| $$ ":" -- parse_literal
    >> (fn ((q, ts), phi) =>
           (* We ignore TFF and THF types for now. *)
-          AQuant (q, map (fn ATerm (s, _) => (s, NONE)) ts, phi))) x
+          AQuant (q, map (fn ATerm ((s, []), _) => (s, NONE)) ts, phi))) x
 
 val parse_tstp_extra_arguments =
   Scan.optional ($$ "," |-- parse_source --| Scan.option ($$ "," |-- skip_term))
@@ -336,7 +337,7 @@
 fun is_same_term subst tm1 tm2 =
   let
     fun do_term_pair _ NONE = NONE
-      | do_term_pair (ATerm (s1, tm1), ATerm (s2, tm2)) (SOME subst) =
+      | do_term_pair (ATerm ((s1, _), tm1), ATerm ((s2, _), tm2)) (SOME subst) =
         case pairself is_tptp_variable (s1, s2) of
           (true, true) =>
           (case AList.lookup (op =) subst s1 of
@@ -358,10 +359,10 @@
   | is_same_formula comm subst (AConn (c1, phis1)) (AConn (c2, phis2)) =
     c1 = c2 andalso length phis1 = length phis2 andalso
     forall (uncurry (is_same_formula comm subst)) (phis1 ~~ phis2)
-  | is_same_formula comm subst (AAtom (tm1 as ATerm ("equal", [tm11, tm12])))
-                    (AAtom tm2) =
+  | is_same_formula comm subst
+        (AAtom (tm1 as ATerm (("equal", []), [tm11, tm12]))) (AAtom tm2) =
     is_same_term subst tm1 tm2 orelse
-    (comm andalso is_same_term subst (ATerm ("equal", [tm12, tm11])) tm2)
+    (comm andalso is_same_term subst (ATerm (("equal", []), [tm12, tm11])) tm2)
   | is_same_formula _ subst (AAtom tm1) (AAtom tm2) = is_same_term subst tm1 tm2
   | is_same_formula _ _ _ _ = false
 
@@ -373,7 +374,7 @@
   problem |> maps snd |> map_filter (matching_formula_line_identifier phi)
           |> try (single o hd) |> the_default []
 
-fun commute_eq (AAtom (ATerm (s, tms))) = AAtom (ATerm (s, rev tms))
+fun commute_eq (AAtom (ATerm ((s, []), tms))) = AAtom (ATerm ((s, []), rev tms))
   | commute_eq _ = raise Fail "expected equation"
 
 (* Syntax: (cnf|fof|tff|thf)\(<num>, <formula_role>,
@@ -416,7 +417,7 @@
               (case phi of
                  AConn (AIff, [phi1 as AAtom _, phi2]) =>
                  Definition_Step (name, phi1, phi2)
-               | AAtom (ATerm ("equal", _)) =>
+               | AAtom (ATerm (("equal", []), _)) =>
                  (* Vampire's equality proxy axiom *)
                  Inference_Step (name, phi, rule, map (rpair []) deps)
                | _ => mk_step ())
@@ -438,7 +439,7 @@
 fun parse_decorated_atom x =
   (parse_atom --| Scan.repeat ($$ "*" || $$ "+" || $$ " ")) x
 
-fun mk_horn ([], []) = AAtom (ATerm ("c_False", []))
+fun mk_horn ([], []) = AAtom (ATerm (("c_False", []), []))
   | mk_horn ([], pos_lits) = foldr1 (uncurry (mk_aconn AOr)) pos_lits
   | mk_horn (neg_lits, []) = mk_anot (foldr1 (uncurry (mk_aconn AAnd)) neg_lits)
   | mk_horn (neg_lits, pos_lits) =
@@ -501,8 +502,8 @@
 
 fun clean_up_atp_proof_dependencies proof = clean_up_dependencies [] proof
 
-fun map_term_names_in_term f (ATerm (s, ts)) =
-  ATerm (f s, map (map_term_names_in_term f) ts)
+fun map_term_names_in_term f (ATerm ((s, tys), ts)) =
+  ATerm ((f s, tys), map (map_term_names_in_term f) ts)
 fun map_term_names_in_formula f (AQuant (q, xs, phi)) =
     AQuant (q, xs, map_term_names_in_formula f phi)
   | map_term_names_in_formula f (AConn (c, phis)) =