src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML
changeset 36966 adc11fb3f3aa
parent 36692 54b64d4ad524
child 37414 d0cea0796295
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML	Mon May 17 10:16:54 2010 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML	Mon May 17 10:18:14 2010 +0200
     1.3 @@ -48,7 +48,7 @@
     1.4      TyLitVar of string * name |
     1.5      TyLitFree of string * name
     1.6    exception CLAUSE of string * term
     1.7 -  val add_type_literals : typ list -> type_literal list
     1.8 +  val type_literals_for_types : typ list -> type_literal list
     1.9    val get_tvar_strs: typ list -> string list
    1.10    datatype arLit =
    1.11        TConsLit of class * string * string list
    1.12 @@ -331,7 +331,8 @@
    1.13    | pred_of_sort (TyLitFree (s, _)) = (s, 1)
    1.14  
    1.15  (*Given a list of sorted type variables, return a list of type literals.*)
    1.16 -fun add_type_literals Ts = fold (union (op =)) (map sorts_on_typs Ts) []
    1.17 +fun type_literals_for_types Ts =
    1.18 +  fold (union (op =)) (map sorts_on_typs Ts) []
    1.19  
    1.20  (*The correct treatment of TFrees like 'a in lemmas (axiom clauses) is not clear.
    1.21    *  Ignoring them leads to unsound proofs, since we do nothing to ensure that 'a
    1.22 @@ -520,7 +521,7 @@
    1.23        dfg_forall vars ("or(" ^ commas lits ^ ")") ^ ",\n" ^
    1.24        string_of_clausename (cls_id,ax_name) ^  ").\n\n";
    1.25  
    1.26 -fun string_of_arity (name, num) =  "(" ^ name ^ "," ^ Int.toString num ^ ")"
    1.27 +fun string_of_arity (name, arity) =  "(" ^ name ^ ", " ^ Int.toString arity ^ ")"
    1.28  
    1.29  fun string_of_preds [] = ""
    1.30    | string_of_preds preds = "predicates[" ^ commas(map string_of_arity preds) ^ "].\n";