# HG changeset patch
# User blanchet
# Date 1305907306 -7200
# Node ID c8d9bce88f89d7ab6901e74576283ff34b5796d4
# Parent  ce269ee43800e0e5878c254110f9428147b1b1d8
name tuning

diff -r ce269ee43800 -r c8d9bce88f89 src/HOL/Tools/Metis/metis_translate.ML
--- a/src/HOL/Tools/Metis/metis_translate.ML	Fri May 20 17:16:13 2011 +0200
+++ b/src/HOL/Tools/Metis/metis_translate.ML	Fri May 20 18:01:46 2011 +0200
@@ -14,11 +14,14 @@
   datatype type_literal =
     TyLitVar of name * name |
     TyLitFree of name * name
-  datatype arLit =
+  datatype arity_literal =
     TConsLit of name * name * name list |
     TVarLit of name * name
   datatype arity_clause =
-    ArityClause of {name: string, conclLit: arLit, premLits: arLit list}
+    ArityClause of
+      {name: string,
+       prem_lits: arity_literal list,
+       concl_lits: arity_literal}
   datatype class_rel_clause =
     ClassRelClause of {name: string, subclass: name, superclass: name}
   datatype combterm =
@@ -274,13 +277,15 @@
 
 (**** Isabelle arities ****)
 
-datatype arLit =
+datatype arity_literal =
   TConsLit of name * name * name list |
   TVarLit of name * name
 
 datatype arity_clause =
-  ArityClause of {name: string, conclLit: arLit, premLits: arLit list}
-
+  ArityClause of
+    {name: string,
+     prem_lits: arity_literal list,
+     concl_lits: arity_literal}
 
 fun gen_TVars 0 = []
   | gen_TVars n = ("T_" ^ string_of_int n) :: gen_TVars (n-1);
@@ -288,7 +293,7 @@
 fun pack_sort(_,[])  = []
   | pack_sort(tvar, "HOL.type"::srt) = pack_sort (tvar, srt)   (*IGNORE sort "type"*)
   | pack_sort(tvar, cls::srt) =
-    (`make_type_class cls, (tvar, tvar)) :: pack_sort (tvar, srt)
+    (`make_type_class cls, `I tvar) :: pack_sort (tvar, srt)
 
 (*Arity of type constructor tcon :: (arg1,...,argN)res*)
 fun make_axiom_arity_clause (tcons, name, (cls,args)) =
@@ -297,10 +302,10 @@
     val tvars_srts = ListPair.zip (tvars, args)
   in
     ArityClause {name = name,
-                 conclLit = TConsLit (`make_type_class cls,
-                                      `make_fixed_type_const tcons,
-                                      tvars ~~ tvars),
-                 premLits = map TVarLit (union_all (map pack_sort tvars_srts))}
+                 prem_lits = map TVarLit (union_all (map pack_sort tvars_srts)),
+                 concl_lits = TConsLit (`make_type_class cls,
+                                        `make_fixed_type_const tcons,
+                                        tvars ~~ tvars)}
   end
 
 
@@ -719,9 +724,10 @@
   | m_arity_cls (TVarLit ((c, _), (s, _))) =
     metis_lit false c [Metis_Term.Var s]
 (*TrueI is returned as the Isabelle counterpart because there isn't any.*)
-fun arity_cls (ArityClause {conclLit, premLits, ...}) =
+fun arity_cls (ArityClause {prem_lits, concl_lits, ...}) =
   (TrueI,
-   Metis_Thm.axiom (Metis_LiteralSet.fromList (map m_arity_cls (conclLit :: premLits))));
+   Metis_Thm.axiom (Metis_LiteralSet.fromList
+                        (map m_arity_cls (concl_lits :: prem_lits))));
 
 (* CLASSREL CLAUSE *)
 fun m_class_rel_cls (subclass, _) (superclass, _) =
diff -r ce269ee43800 -r c8d9bce88f89 src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Fri May 20 17:16:13 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Fri May 20 18:01:46 2011 +0200
@@ -922,13 +922,13 @@
   | fo_literal_from_arity_literal (TVarLit (c, sort)) =
     (false, ATerm (c, [ATerm (sort, [])]))
 
-fun formula_line_for_arity_clause (ArityClause {name, conclLit, premLits,
+fun formula_line_for_arity_clause (ArityClause {name, prem_lits, concl_lits,
                                                 ...}) =
   Formula (arity_clause_prefix ^ ascii_of name, Axiom,
            mk_ahorn (map (formula_from_fo_literal o apfst not
-                          o fo_literal_from_arity_literal) premLits)
+                          o fo_literal_from_arity_literal) prem_lits)
                     (formula_from_fo_literal
-                         (fo_literal_from_arity_literal conclLit))
+                         (fo_literal_from_arity_literal concl_lits))
            |> close_formula_universally, intro_info, NONE)
 
 fun formula_line_for_conjecture ctxt nonmono_Ts type_sys