1.1 --- a/src/HOL/Tools/ATP/atp_problem.ML	Thu Sep 16 11:12:08 2010 +0200
     1.2 +++ b/src/HOL/Tools/ATP/atp_problem.ML	Thu Sep 16 11:59:45 2010 +0200
     1.3 @@ -14,6 +14,7 @@
     1.4      AQuant of quantifier * 'a list * ('a, 'b) formula |
     1.5      AConn of connective * ('a, 'b) formula list |
     1.6      AAtom of 'b
     1.7 +  type 'a uniform_formula = ('a, 'a fo_term) formula
     1.8  
     1.9    datatype kind = Axiom | Hypothesis | Conjecture
    1.10    datatype 'a problem_line = Fof of string * kind * ('a, 'a fo_term) formula
    1.11 @@ -41,6 +42,7 @@
    1.12    AQuant of quantifier * 'a list * ('a, 'b) formula |
    1.13    AConn of connective * ('a, 'b) formula list |
    1.14    AAtom of 'b
    1.15 +type 'a uniform_formula = ('a, 'a fo_term) formula
    1.16  
    1.17  datatype kind = Axiom | Hypothesis | Conjecture
    1.18  datatype 'a problem_line = Fof of string * kind * ('a, 'a fo_term) formula