# HG changeset patch
# User blanchet
# Date 1279739626 -7200
# Node ID ff56c361d75bf6335327d2907816d8d5a2b2569e
# Parent  1e846be00ddf5db0e4b77866763d56f8655c3245
renamed "HOLClause" to "FOLClause" -- it's really a FOL clause with combinators

diff -r 1e846be00ddf -r ff56c361d75b src/HOL/Tools/ATP_Manager/atp_systems.ML
--- a/src/HOL/Tools/ATP_Manager/atp_systems.ML	Wed Jul 21 18:13:15 2010 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_systems.ML	Wed Jul 21 21:13:46 2010 +0200
@@ -140,7 +140,7 @@
       (pol andalso c = "c_True") orelse
       (not pol andalso c = "c_False")
   | is_true_literal _ = false;
-fun is_tautology (HOLClause {literals,...}) = exists is_true_literal literals
+fun is_tautology (FOLClause {literals,...}) = exists is_true_literal literals
 
 (* making axiom and conjecture clauses *)
 fun make_clause thy (clause_id, axiom_name, kind, th) skolems =
@@ -152,7 +152,7 @@
       raise TRIVIAL ()
     else
       (skolems,
-       HOLClause {clause_id = clause_id, axiom_name = axiom_name, th = th,
+       FOLClause {clause_id = clause_id, axiom_name = axiom_name, th = th,
                   kind = kind, literals = lits, ctypes_sorts = ctypes_sorts})
   end
 
@@ -181,7 +181,7 @@
   | count_combterm (CombVar _) = I
   | count_combterm (CombApp (t1, t2)) = count_combterm t1 #> count_combterm t2
 fun count_literal (Literal (_, t)) = count_combterm t
-fun count_clause (HOLClause {literals, ...}) = fold count_literal literals
+fun count_clause (FOLClause {literals, ...}) = fold count_literal literals
 
 fun cnf_helper_thms thy raw =
   map (`Thm.get_name_hint)
diff -r 1e846be00ddf -r ff56c361d75b src/HOL/Tools/Sledgehammer/metis_clauses.ML
--- a/src/HOL/Tools/Sledgehammer/metis_clauses.ML	Wed Jul 21 18:13:15 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/metis_clauses.ML	Wed Jul 21 21:13:46 2010 +0200
@@ -29,8 +29,8 @@
     CombVar of name * combtyp |
     CombApp of combterm * combterm
   datatype literal = Literal of bool * combterm
-  datatype hol_clause =
-    HOLClause of {clause_id: int, axiom_name: string, th: thm, kind: kind,
+  datatype fol_clause =
+    FOLClause of {clause_id: int, axiom_name: string, th: thm, kind: kind,
                   literals: literal list, ctypes_sorts: typ list}
 
   val type_wrapper_name : string
@@ -363,8 +363,8 @@
 
 datatype literal = Literal of bool * combterm
 
-datatype hol_clause =
-  HOLClause of {clause_id: int, axiom_name: string, th: thm, kind: kind,
+datatype fol_clause =
+  FOLClause of {clause_id: int, axiom_name: string, th: thm, kind: kind,
                 literals: literal list, ctypes_sorts: typ list}
 
 (*********************************************************************)
diff -r 1e846be00ddf -r ff56c361d75b src/HOL/Tools/Sledgehammer/sledgehammer_tptp_format.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_tptp_format.ML	Wed Jul 21 18:13:15 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_tptp_format.ML	Wed Jul 21 21:13:46 2010 +0200
@@ -9,12 +9,12 @@
 sig
   type classrel_clause = Metis_Clauses.classrel_clause
   type arity_clause = Metis_Clauses.arity_clause
-  type hol_clause = Metis_Clauses.hol_clause
+  type fol_clause = Metis_Clauses.fol_clause
   type name_pool = string Symtab.table * string Symtab.table
 
   val write_tptp_file :
     theory -> bool -> bool -> bool -> Path.T
-    -> hol_clause list * hol_clause list * hol_clause list * hol_clause list
+    -> fol_clause list * fol_clause list * fol_clause list * fol_clause list
        * classrel_clause list * arity_clause list
     -> name_pool option * int
 end;
@@ -154,13 +154,13 @@
     (pos, ATerm (class, [ATerm (name, [])]))
 
 fun atp_literals_for_axiom full_types
-        (HOLClause {literals, ctypes_sorts, ...}) =
+                           (FOLClause {literals, ctypes_sorts, ...}) =
   map (atp_literal_for_literal full_types) literals @
   map (atp_literal_for_type_literal false)
       (type_literals_for_types ctypes_sorts)
 
 fun problem_line_for_axiom full_types
-        (clause as HOLClause {axiom_name, clause_id, kind, ...}) =
+        (clause as FOLClause {axiom_name, clause_id, kind, ...}) =
   Cnf (hol_ident axiom_name clause_id, kind,
        atp_literals_for_axiom full_types clause)
 
@@ -181,11 +181,11 @@
        map atp_literal_for_arity_literal (conclLit :: premLits))
 
 fun problem_line_for_conjecture full_types
-        (clause as HOLClause {axiom_name, clause_id, kind, literals, ...}) =
+        (clause as FOLClause {axiom_name, clause_id, kind, literals, ...}) =
   Cnf (hol_ident axiom_name clause_id, kind,
        map (atp_literal_for_literal full_types) literals)
 
-fun atp_free_type_literals_for_conjecture (HOLClause {ctypes_sorts, ...}) =
+fun atp_free_type_literals_for_conjecture (FOLClause {ctypes_sorts, ...}) =
   map (atp_literal_for_type_literal true) (type_literals_for_types ctypes_sorts)
 
 fun problem_line_for_free_type lit = Cnf ("tfree_tcs", Conjecture, [lit])