rename "classrel" to "class_rel"

--- a/src/HOL/Tools/ATP_Manager/atp_systems.ML	Wed Jul 21 21:14:26 2010 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_systems.ML	Wed Jul 21 21:14:47 2010 +0200
@@ -233,10 +233,11 @@
     val helper_clauses =
       get_helper_clauses thy is_FO full_types conjectures extra_cls
     val (supers', arity_clauses) = make_arity_clauses thy tycons supers
-    val classrel_clauses = make_classrel_clauses thy subs supers'
+    val class_rel_clauses = make_class_rel_clauses thy subs supers'
   in
     (Vector.fromList clnames,
-      (conjectures, axiom_clauses, extra_clauses, helper_clauses, classrel_clauses, arity_clauses))
+      (conjectures, axiom_clauses, extra_clauses, helper_clauses,
+       class_rel_clauses, arity_clauses))
   end
 
 

--- a/src/HOL/Tools/Sledgehammer/metis_clauses.ML	Wed Jul 21 21:14:26 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/metis_clauses.ML	Wed Jul 21 21:14:47 2010 +0200
@@ -18,7 +18,7 @@
     TVarLit of name * name
   datatype arity_clause = ArityClause of
    {axiom_name: string, conclLit: arLit, premLits: arLit list}
-  datatype classrel_clause = ClassrelClause of
+  datatype class_rel_clause = ClassRelClause of
    {axiom_name: string, subclass: name, superclass: name}
   datatype combtyp =
     CombTVar of name |
@@ -59,7 +59,7 @@
   val is_skolem_const_name: string -> bool
   val num_type_args: theory -> string -> int
   val type_literals_for_types : typ list -> type_literal list
-  val make_classrel_clauses: theory -> class list -> class list -> classrel_clause list
+  val make_class_rel_clauses: theory -> class list -> class list -> class_rel_clause list
   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
@@ -85,7 +85,7 @@
 val tvar_prefix = "T_";
 val tfree_prefix = "t_";
 
-val classrel_clause_prefix = "clsrel_";
+val class_rel_clause_prefix = "clsrel_";
 
 val const_prefix = "c_";
 val type_const_prefix = "tc_";
@@ -288,8 +288,8 @@
 
 (**** Isabelle class relations ****)
 
-datatype classrel_clause =
-  ClassrelClause of {axiom_name: string, subclass: name, superclass: name}
+datatype class_rel_clause =
+  ClassRelClause of {axiom_name: string, subclass: name, superclass: name}
 
 (*Generate all pairs (sub,super) such that sub is a proper subclass of super in theory thy.*)
 fun class_pairs _ [] _ = []
@@ -300,14 +300,14 @@
         fun add_supers sub = fold (add_super sub) supers
       in fold add_supers subs [] end
 
-fun make_classrel_clause (sub,super) =
-  ClassrelClause {axiom_name = classrel_clause_prefix ^ ascii_of sub ^ "_" ^
+fun make_class_rel_clause (sub,super) =
+  ClassRelClause {axiom_name = class_rel_clause_prefix ^ ascii_of sub ^ "_" ^
                                ascii_of super,
                   subclass = `make_type_class sub,
                   superclass = `make_type_class super};
 
-fun make_classrel_clauses thy subs supers =
-  map make_classrel_clause (class_pairs thy subs supers);
+fun make_class_rel_clauses thy subs supers =
+  map make_class_rel_clause (class_pairs thy subs supers);
 
 
 (** Isabelle arities **)

--- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML	Wed Jul 21 21:14:26 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML	Wed Jul 21 21:14:47 2010 +0200
@@ -170,11 +170,11 @@
 
 (* CLASSREL CLAUSE *)
 
-fun m_classrel_cls (subclass, _) (superclass, _) =
+fun m_class_rel_cls (subclass, _) (superclass, _) =
   [metis_lit false subclass [Metis.Term.Var "T"], metis_lit true superclass [Metis.Term.Var "T"]];
 
-fun classrel_cls (ClassrelClause {subclass, superclass, ...}) =
-  (TrueI, Metis.Thm.axiom (Metis.LiteralSet.fromList (m_classrel_cls subclass superclass)));
+fun class_rel_cls (ClassRelClause {subclass, superclass, ...}) =
+  (TrueI, Metis.Thm.axiom (Metis.LiteralSet.fromList (m_class_rel_cls subclass superclass)));
 
 (* ------------------------------------------------------------------------- *)
 (* FOL to HOL  (Metis to Isabelle)                                           *)
@@ -606,8 +606,8 @@
       val supers = tvar_classes_of_terms tms
       and tycons = type_consts_of_terms thy tms
       val (supers', arity_clauses) = make_arity_clauses thy tycons supers
-      val classrel_clauses = make_classrel_clauses thy subs supers'
-  in  map classrel_cls classrel_clauses @ map arity_cls arity_clauses
+      val class_rel_clauses = make_class_rel_clauses thy subs supers'
+  in  map class_rel_cls class_rel_clauses @ map arity_cls arity_clauses
   end;
 
 (* ------------------------------------------------------------------------- *)

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_tptp_format.ML	Wed Jul 21 21:14:26 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_tptp_format.ML	Wed Jul 21 21:14:47 2010 +0200
@@ -7,7 +7,7 @@
 
 signature SLEDGEHAMMER_TPTP_FORMAT =
 sig
-  type classrel_clause = Metis_Clauses.classrel_clause
+  type class_rel_clause = Metis_Clauses.class_rel_clause
   type arity_clause = Metis_Clauses.arity_clause
   type fol_clause = Metis_Clauses.fol_clause
   type name_pool = string Symtab.table * string Symtab.table
@@ -15,7 +15,7 @@
   val write_tptp_file :
     theory -> bool -> bool -> bool -> Path.T
     -> fol_clause list * fol_clause list * fol_clause list * fol_clause list
-       * classrel_clause list * arity_clause list
+       * class_rel_clause list * arity_clause list
     -> name_pool option * int
 end;
 
@@ -164,8 +164,8 @@
   Cnf (hol_ident axiom_name clause_id, kind,
        atp_literals_for_axiom full_types clause)
 
-fun problem_line_for_classrel
-        (ClassrelClause {axiom_name, subclass, superclass, ...}) =
+fun problem_line_for_class_rel
+        (ClassRelClause {axiom_name, subclass, superclass, ...}) =
   let val ty_arg = ATerm (("T", "T"), []) in
     Cnf (ascii_of axiom_name, Axiom, [(false, ATerm (subclass, [ty_arg])),
                                       (true, ATerm (superclass, [ty_arg]))])
@@ -303,17 +303,17 @@
 
 fun write_tptp_file thy readable_names full_types explicit_apply file
                     (conjectures, axiom_clauses, extra_clauses, helper_clauses,
-                     classrel_clauses, arity_clauses) =
+                     class_rel_clauses, arity_clauses) =
   let
     val axiom_lines = map (problem_line_for_axiom full_types) axiom_clauses
-    val classrel_lines = map problem_line_for_classrel classrel_clauses
+    val class_rel_lines = map problem_line_for_class_rel class_rel_clauses
     val arity_lines = map problem_line_for_arity arity_clauses
     val helper_lines = map (problem_line_for_axiom full_types) helper_clauses
     val conjecture_lines =
       map (problem_line_for_conjecture full_types) conjectures
     val tfree_lines = problem_lines_for_free_types conjectures
     val problem = [("Relevant facts", axiom_lines),
-                   ("Class relationships", classrel_lines),
+                   ("Class relationships", class_rel_lines),
                    ("Arity declarations", arity_lines),
                    ("Helper facts", helper_lines),
                    ("Conjectures", conjecture_lines),
@@ -321,7 +321,7 @@
                   |> repair_problem thy full_types explicit_apply
     val (problem, pool) = nice_problem problem (empty_name_pool readable_names)
     val conjecture_offset =
-      length axiom_lines + length classrel_lines + length arity_lines
+      length axiom_lines + length class_rel_lines + length arity_lines
       + length helper_lines
     val _ = File.write_list file (strings_for_problem problem)
   in (pool, conjecture_offset) end