src/HOL/Tools/ATP/atp_translate.ML

 
   datatype arity_literal =
     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}
-
-  datatype class_rel_clause =
-    ClassRelClause of {name: string, subclass: name, superclass: name}
+  type arity_clause =
+    {name: string,
+     prem_lits: arity_literal list,
+     concl_lits: arity_literal}
+
+  type class_rel_clause =
+    {name: string,
+     subclass: name,
+     superclass: name}
 
   datatype combterm =
     CombConst of name * typ * typ list |
     CombVar of name * typ |
     CombApp of combterm * combterm

   | pack_sort (tvar, "HOL.type" :: srt) =
     pack_sort (tvar, srt) (* IGNORE sort "type" *)
   | 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)) =
   let
     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 _ _ (_, []) = []
   | arity_clause seen n (tcons, ("HOL.type",_)::ars) =  (*ignore*)
       arity_clause seen n (tcons,ars)

   iter_type_class_pairs thy tycons ##> multi_arity_clause
 
 
 (** 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 _ [] _ = []
   | class_pairs thy subs supers =
       let

         fun add_super sub super = class_less (sub, super) ? cons (sub, super)
         fun add_supers sub = fold (add_super sub) supers
       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);
 
 datatype combterm =

              Intro => intro_info
            | Elim => elim_info
            | 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])),
                                AAtom (ATerm (superclass, [ty_arg]))])
              |> close_formula_universally, intro_info, NONE)

 fun fo_literal_from_arity_literal (TConsLit (c, t, args)) =
     (true, ATerm (c, [ATerm (t, map (fn arg => ATerm (arg, [])) args)]))
   | 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)
                     (formula_from_fo_literal
                          (fo_literal_from_arity_literal concl_lits))