# HG changeset patch
# User blanchet
# Date 1306852716 -7200
# Node ID 4dce7f2bb59fb5d541068db404ae1d6727a79fb5
# Parent  0a2f5b86bdd7de6dc433fbcf20f7aad79ee28d7b
tuning

diff -r 0a2f5b86bdd7 -r 4dce7f2bb59f src/HOL/Tools/ATP/atp_translate.ML
--- a/src/HOL/Tools/ATP/atp_translate.ML	Tue May 31 16:38:36 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_translate.ML	Tue May 31 16:38:36 2011 +0200
@@ -23,14 +23,15 @@
     TConsLit of name * name * name list |
     TVarLit of name * name
 
-  datatype arity_clause =
-    ArityClause of
-      {name: string,
-       prem_lits: arity_literal list,
-       concl_lits: arity_literal}
+  type arity_clause =
+    {name: string,
+     prem_lits: arity_literal list,
+     concl_lits: arity_literal}
 
-  datatype class_rel_clause =
-    ClassRelClause of {name: string, subclass: name, superclass: name}
+  type class_rel_clause =
+    {name: string,
+     subclass: name,
+     superclass: name}
 
   datatype combterm =
     CombConst of name * typ * typ list |
@@ -341,11 +342,10 @@
   | pack_sort (tvar, cls :: srt) =
     (`make_type_class cls, `I tvar) :: pack_sort (tvar, srt)
 
-datatype arity_clause =
-  ArityClause of
-    {name: string,
-     prem_lits: arity_literal list,
-     concl_lits: arity_literal}
+type arity_clause =
+  {name: string,
+   prem_lits: arity_literal list,
+   concl_lits: arity_literal}
 
 (* Arity of type constructor "tcon :: (arg1, ..., argN) res" *)
 fun make_axiom_arity_clause (tcons, name, (cls, args)) =
@@ -353,11 +353,11 @@
     val tvars = gen_TVars (length args)
     val tvars_srts = ListPair.zip (tvars, args)
   in
-    ArityClause {name = name,
-                 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)}
+    {name = name,
+     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
 
 fun arity_clause _ _ (_, []) = []
@@ -401,8 +401,10 @@
 
 (** Isabelle class relations **)
 
-datatype class_rel_clause =
-  ClassRelClause of {name: string, subclass: name, superclass: name}
+type class_rel_clause =
+  {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 _ [] _ = []
@@ -414,9 +416,9 @@
       in fold add_supers subs [] end
 
 fun make_class_rel_clause (sub,super) =
-  ClassRelClause {name = sub ^ "_" ^ super,
-                  subclass = `make_type_class sub,
-                  superclass = `make_type_class super}
+  {name = sub ^ "_" ^ super,
+   subclass = `make_type_class sub,
+   superclass = `make_type_class super}
 
 fun make_class_rel_clauses thy subs supers =
   map make_class_rel_clause (class_pairs thy subs supers);
@@ -1461,8 +1463,8 @@
            | Simp => simp_info
            | _ => NONE)
 
-fun formula_line_for_class_rel_clause
-        (ClassRelClause {name, subclass, superclass, ...}) =
+fun formula_line_for_class_rel_clause ({name, subclass, superclass, ...}
+                                       : class_rel_clause) =
   let val ty_arg = ATerm (`I "T", []) in
     Formula (class_rel_clause_prefix ^ ascii_of name, Axiom,
              AConn (AImplies, [AAtom (ATerm (subclass, [ty_arg])),
@@ -1475,8 +1477,8 @@
   | fo_literal_from_arity_literal (TVarLit (c, sort)) =
     (false, ATerm (c, [ATerm (sort, [])]))
 
-fun formula_line_for_arity_clause
-        (ArityClause {name, prem_lits, concl_lits, ...}) =
+fun formula_line_for_arity_clause ({name, prem_lits, concl_lits, ...}
+                                   : arity_clause) =
   Formula (arity_clause_prefix ^ ascii_of name, Axiom,
            mk_ahorn (map (formula_from_fo_literal o apfst not
                           o fo_literal_from_arity_literal) prem_lits)
diff -r 0a2f5b86bdd7 -r 4dce7f2bb59f src/HOL/Tools/Metis/metis_translate.ML
--- a/src/HOL/Tools/Metis/metis_translate.ML	Tue May 31 16:38:36 2011 +0200
+++ b/src/HOL/Tools/Metis/metis_translate.ML	Tue May 31 16:38:36 2011 +0200
@@ -272,7 +272,7 @@
   | 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 {prem_lits, concl_lits, ...}) =
+fun arity_cls ({prem_lits, concl_lits, ...} : arity_clause) =
   (TrueI,
    Metis_Thm.axiom (Metis_LiteralSet.fromList
                         (map m_arity_cls (concl_lits :: prem_lits))));
@@ -280,7 +280,7 @@
 (* CLASSREL CLAUSE *)
 fun m_class_rel_cls (subclass, _) (superclass, _) =
   [metis_lit false subclass [Metis_Term.Var "T"], metis_lit true superclass [Metis_Term.Var "T"]];
-fun class_rel_cls (ClassRelClause {subclass, superclass, ...}) =
+fun class_rel_cls ({subclass, superclass, ...} : class_rel_clause) =
   (TrueI, Metis_Thm.axiom (Metis_LiteralSet.fromList (m_class_rel_cls subclass superclass)));
 
 fun type_ext thy tms =