src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML
changeset 36170 0cdb76723c88
parent 36169 27b1cc58715e
child 36218 0e4a01f3e7d3
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML	Fri Apr 16 14:48:34 2010 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML	Fri Apr 16 15:49:13 2010 +0200
     1.3 @@ -41,7 +41,8 @@
     1.4      TyVar of name |
     1.5      TyFree of name |
     1.6      TyConstr of name * fol_type list
     1.7 -  val string_of_fol_type : fol_type -> string
     1.8 +  val string_of_fol_type :
     1.9 +    fol_type -> name_pool option -> string * name_pool option
    1.10    datatype type_literal = LTVar of string * string | LTFree of string * string
    1.11    exception CLAUSE of string * term
    1.12    val add_typs : typ list -> type_literal list
    1.13 @@ -220,7 +221,8 @@
    1.14  fun empty_name_pool debug = if debug then SOME (`I Symtab.empty) else NONE
    1.15  
    1.16  fun pool_map f xs =
    1.17 -  fold (fn x => fn (ys, pool) => f x pool |>> (fn y => y :: ys)) xs o pair []
    1.18 +  fold_rev (fn x => fn (ys, pool) => f x pool |>> (fn y => y :: ys)) xs
    1.19 +  o pair []
    1.20  
    1.21  fun add_nice_name full_name nice_prefix j the_pool =
    1.22    let
    1.23 @@ -283,20 +285,19 @@
    1.24    TyFree of name |
    1.25    TyConstr of name * fol_type list
    1.26  
    1.27 -fun string_of_fol_type (TyVar (s, _)) = s
    1.28 -  | string_of_fol_type (TyFree (s, _)) = s
    1.29 -  | string_of_fol_type (TyConstr ((tcon, _), tps)) =
    1.30 -      tcon ^ (paren_pack (map string_of_fol_type tps));
    1.31 +fun string_of_fol_type (TyVar sp) pool = nice_name sp pool
    1.32 +  | string_of_fol_type (TyFree sp) pool = nice_name sp pool
    1.33 +  | string_of_fol_type (TyConstr (sp, tys)) pool =
    1.34 +    let
    1.35 +      val (s, pool) = nice_name sp pool
    1.36 +      val (ss, pool) = pool_map string_of_fol_type tys pool
    1.37 +    in (s ^ paren_pack ss, pool) end
    1.38  
    1.39  (*First string is the type class; the second is a TVar or TFfree*)
    1.40  datatype type_literal = LTVar of string * string | LTFree of string * string;
    1.41  
    1.42  exception CLAUSE of string * term;
    1.43  
    1.44 -fun atomic_type (TFree (a,_)) = TyFree (`make_fixed_type_var a)
    1.45 -  | atomic_type (TVar (x, _)) =
    1.46 -    TyVar (make_schematic_type_var x, string_of_indexname x)
    1.47 -
    1.48  (*Make literals for sorted type variables*)
    1.49  fun sorts_on_typs_aux (_, [])   = []
    1.50    | sorts_on_typs_aux ((x,i),  s::ss) =
    1.51 @@ -335,8 +336,6 @@
    1.52  
    1.53  (**** Isabelle arities ****)
    1.54  
    1.55 -exception ARCLAUSE of string;
    1.56 -
    1.57  datatype arLit = TConsLit of class * string * string list
    1.58                 | TVarLit of class * string;
    1.59