# HG changeset patch
# User blanchet
# Date 1279739647 -7200
# Node ID 8edbaf6ba4058121799e5b391fe7f983bb36f140
# Parent  ff56c361d75bf6335327d2907816d8d5a2b2569e
renamed "Literal" to "FOLLiteral"

diff -r ff56c361d75b -r 8edbaf6ba405 src/HOL/Tools/ATP_Manager/atp_systems.ML
--- a/src/HOL/Tools/ATP_Manager/atp_systems.ML	Wed Jul 21 21:13:46 2010 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_systems.ML	Wed Jul 21 21:14:07 2010 +0200
@@ -133,10 +133,10 @@
 fun subtract_cls ax_clauses =
   filter_out (Termtab.defined (make_clause_table ax_clauses) o prop_of)
 
-fun is_false_literal (Literal (pos, CombConst ((c, _), _, _))) =
+fun is_false_literal (FOLLiteral (pos, CombConst ((c, _), _, _))) =
       (pos andalso c = "c_False") orelse (not pos andalso c = "c_True")
   | is_false_literal _ = false
-fun is_true_literal (Literal (pol, CombConst ((c, _), _, _))) =
+fun is_true_literal (FOLLiteral (pol, CombConst ((c, _), _, _))) =
       (pol andalso c = "c_True") orelse
       (not pol andalso c = "c_False")
   | is_true_literal _ = false;
@@ -180,7 +180,7 @@
     Symtab.map_entry c (Integer.add 1)
   | 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_literal (FOLLiteral (_, t)) = count_combterm t
 fun count_clause (FOLClause {literals, ...}) = fold count_literal literals
 
 fun cnf_helper_thms thy raw =
diff -r ff56c361d75b -r 8edbaf6ba405 src/HOL/Tools/Sledgehammer/metis_clauses.ML
--- a/src/HOL/Tools/Sledgehammer/metis_clauses.ML	Wed Jul 21 21:13:46 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/metis_clauses.ML	Wed Jul 21 21:14:07 2010 +0200
@@ -28,10 +28,10 @@
     CombConst of name * combtyp * combtyp list (* Const and Free *) |
     CombVar of name * combtyp |
     CombApp of combterm * combterm
-  datatype literal = Literal of bool * combterm
+  datatype fol_literal = FOLLiteral of bool * combterm
   datatype fol_clause =
     FOLClause of {clause_id: int, axiom_name: string, th: thm, kind: kind,
-                  literals: literal list, ctypes_sorts: typ list}
+                  literals: fol_literal list, ctypes_sorts: typ list}
 
   val type_wrapper_name : string
   val schematic_var_prefix: string
@@ -63,7 +63,7 @@
   val make_arity_clauses: theory -> string list -> class list -> class list * arity_clause list
   val type_of_combterm : combterm -> combtyp
   val strip_combterm_comb : combterm -> combterm * combterm list
-  val literals_of_term : theory -> term -> literal list * typ list
+  val literals_of_term : theory -> term -> fol_literal list * typ list
   val conceal_skolem_terms :
     int -> (string * term) list -> term -> (string * term) list * term
   val reveal_skolem_terms : (string * term) list -> term -> term
@@ -361,11 +361,11 @@
   CombVar of name * combtyp |
   CombApp of combterm * combterm
 
-datatype literal = Literal of bool * combterm
+datatype fol_literal = FOLLiteral of bool * combterm
 
 datatype fol_clause =
   FOLClause of {clause_id: int, axiom_name: string, th: thm, kind: kind,
-                literals: literal list, ctypes_sorts: typ list}
+                literals: fol_literal list, ctypes_sorts: typ list}
 
 (*********************************************************************)
 (* convert a clause with type Term.term to a clause with type clause *)
@@ -439,7 +439,7 @@
     literals_of_term1 (literals_of_term1 args thy P) thy Q
   | literals_of_term1 (lits, ts) thy P =
     let val ((pred, ts'), pol) = predicate_of thy (P, true) in
-      (Literal (pol, pred) :: lits, union (op =) ts ts')
+      (FOLLiteral (pol, pred) :: lits, union (op =) ts ts')
     end
 val literals_of_term = literals_of_term1 ([], [])
 
diff -r ff56c361d75b -r 8edbaf6ba405 src/HOL/Tools/Sledgehammer/metis_tactics.ML
--- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML	Wed Jul 21 21:13:46 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML	Wed Jul 21 21:14:07 2010 +0200
@@ -103,21 +103,21 @@
        wrap_type (Metis.Term.Fn(".", map hol_term_to_fol_FT [tm1,tm2]),
                   type_of_combterm tm);
 
-fun hol_literal_to_fol FO (Literal (pol, tm)) =
+fun hol_literal_to_fol FO (FOLLiteral (pos, tm)) =
       let val (CombConst((p, _), _, tys), tms) = strip_combterm_comb tm
           val tylits = if p = "equal" then [] else map hol_type_to_fol tys
           val lits = map hol_term_to_fol_FO tms
-      in metis_lit pol (fn_isa_to_met p) (tylits @ lits) end
-  | hol_literal_to_fol HO (Literal (pol, tm)) =
+      in metis_lit pos (fn_isa_to_met p) (tylits @ lits) end
+  | hol_literal_to_fol HO (FOLLiteral (pos, tm)) =
      (case strip_combterm_comb tm of
           (CombConst(("equal", _), _, _), tms) =>
-            metis_lit pol "=" (map hol_term_to_fol_HO tms)
-        | _ => metis_lit pol "{}" [hol_term_to_fol_HO tm])   (*hBOOL*)
-  | hol_literal_to_fol FT (Literal (pol, tm)) =
+            metis_lit pos "=" (map hol_term_to_fol_HO tms)
+        | _ => metis_lit pos "{}" [hol_term_to_fol_HO tm])   (*hBOOL*)
+  | hol_literal_to_fol FT (FOLLiteral (pos, tm)) =
      (case strip_combterm_comb tm of
           (CombConst(("equal", _), _, _), tms) =>
-            metis_lit pol "=" (map hol_term_to_fol_FT tms)
-        | _ => metis_lit pol "{}" [hol_term_to_fol_FT tm])   (*hBOOL*);
+            metis_lit pos "=" (map hol_term_to_fol_FT tms)
+        | _ => metis_lit pos "{}" [hol_term_to_fol_FT tm])   (*hBOOL*);
 
 fun literals_of_hol_term thy mode t =
       let val (lits, types_sorts) = literals_of_term thy t
diff -r ff56c361d75b -r 8edbaf6ba405 src/HOL/Tools/Sledgehammer/sledgehammer_tptp_format.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_tptp_format.ML	Wed Jul 21 21:13:46 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_tptp_format.ML	Wed Jul 21 21:14:07 2010 +0200
@@ -145,7 +145,7 @@
     else t
   end
 
-fun atp_literal_for_literal full_types (Literal (pos, t)) =
+fun atp_literal_for_literal full_types (FOLLiteral (pos, t)) =
   (pos, atp_term_for_combterm full_types true t)
 
 fun atp_literal_for_type_literal pos (TyLitVar (class, name)) =