src/HOL/Tools/res_hol_clause.ML
changeset 24940 8f9dea697b8d
parent 24937 340523598914
child 24943 5f5679e2ec2f
     1.1 --- a/src/HOL/Tools/res_hol_clause.ML	Tue Oct 09 19:48:55 2007 +0200
     1.2 +++ b/src/HOL/Tools/res_hol_clause.ML	Wed Oct 10 10:50:11 2007 +0200
     1.3 @@ -28,7 +28,7 @@
     1.4      | CombApp of combterm * combterm
     1.5    datatype literal = Literal of polarity * combterm
     1.6    val strip_comb: combterm -> combterm * combterm list
     1.7 -  val literals_of_term: theory -> term -> literal list * (ResClause.typ_var * sort) list
     1.8 +  val literals_of_term: theory -> term -> literal list * typ list
     1.9    val tptp_write_file: theory -> bool -> thm list -> string ->
    1.10      (thm * (axiom_name * clause_id)) list * ResClause.classrelClause list *
    1.11        ResClause.arityClause list -> string list -> axiom_name list
    1.12 @@ -97,7 +97,7 @@
    1.13                      th: thm,
    1.14                      kind: RC.kind,
    1.15                      literals: literal list,
    1.16 -                    ctypes_sorts: (RC.typ_var * Term.sort) list};
    1.17 +                    ctypes_sorts: typ list};
    1.18  
    1.19  
    1.20  (*********************************************************************)
    1.21 @@ -120,9 +120,9 @@
    1.22        let val (folTypes,ts) = types_of Ts
    1.23        in  (RC.Comp(RC.make_fixed_type_const a, folTypes), ts)  end
    1.24    | type_of (tp as (TFree(a,s))) =
    1.25 -      (RC.AtomF (RC.make_fixed_type_var a), [RC.mk_typ_var_sort tp])
    1.26 +      (RC.AtomF (RC.make_fixed_type_var a), [tp])
    1.27    | type_of (tp as (TVar(v,s))) =
    1.28 -      (RC.AtomV (RC.make_schematic_type_var v), [RC.mk_typ_var_sort tp])
    1.29 +      (RC.AtomV (RC.make_schematic_type_var v), [tp])
    1.30  and types_of Ts =
    1.31        let val (folTyps,ts) = ListPair.unzip (map type_of Ts)
    1.32        in  (folTyps, RC.union_all ts)  end;