src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML

   val class_rel_clause_prefix : string
   val arity_clause_prefix : string
   val tfrees_name : string
   val prepare_problem :
     Proof.context -> bool -> bool -> bool -> bool -> term list -> term
-    -> ((string * bool) * thm) list
-    -> string problem * string Symtab.table * int * (string * bool) vector
+    -> ((string * 'a) * thm) list
+    -> string problem * string Symtab.table * int * (string * 'a) vector
 end;
 
 structure Sledgehammer_Translate : SLEDGEHAMMER_TRANSLATE =
 struct
 

 val tfrees_name = "tfrees"
 
 (* Freshness almost guaranteed! *)
 val sledgehammer_weak_prefix = "Sledgehammer:"
 
-datatype fol_formula =
-  FOLFormula of {name: string,
-                 kind: kind,
-                 combformula: (name, combterm) formula,
-                 ctypes_sorts: typ list}
+type fol_formula =
+  {name: string,
+   kind: kind,
+   combformula: (name, combterm) formula,
+   ctypes_sorts: typ list}
 
 fun mk_anot phi = AConn (ANot, [phi])
 fun mk_aconn c phi1 phi2 = AConn (c, [phi1, phi2])
 fun mk_ahorn [] phi = phi
   | mk_ahorn (phi :: phis) psi =

               |> perhaps (try (HOLogic.dest_Trueprop))
               |> introduce_combinators_in_term ctxt kind
               |> kind <> Axiom ? freeze_term
     val (combformula, ctypes_sorts) = combformula_for_prop thy t []
   in
-    FOLFormula {name = name, combformula = combformula, kind = kind,
-                ctypes_sorts = ctypes_sorts}
-  end
-
-fun make_axiom ctxt presimp ((name, chained), th) =
+    {name = name, combformula = combformula, kind = kind,
+     ctypes_sorts = ctypes_sorts}
+  end
+
+fun make_axiom ctxt presimp ((name, loc), th) =
   case make_formula ctxt presimp name Axiom (prop_of th) of
-    FOLFormula {combformula = AAtom (CombConst (("c_True", _), _, _)), ...} =>
-    NONE
-  | formula => SOME ((name, chained), formula)
+    {combformula = AAtom (CombConst (("c_True", _), _, _)), ...} => NONE
+  | formula => SOME ((name, loc), formula)
 fun make_conjecture ctxt ts =
   let val last = length ts - 1 in
     map2 (fn j => make_formula ctxt true (Int.toString j)
                                (if j = last then Conjecture else Hypothesis))
          (0 upto last) ts

   | count_combterm (CombVar _) = I
   | count_combterm (CombApp (t1, t2)) = fold count_combterm [t1, t2]
 fun count_combformula (AQuant (_, _, phi)) = count_combformula phi
   | count_combformula (AConn (_, phis)) = fold count_combformula phis
   | count_combformula (AAtom tm) = count_combterm tm
-fun count_fol_formula (FOLFormula {combformula, ...}) =
+fun count_fol_formula ({combformula, ...} : fol_formula) =
   count_combformula combformula
 
 val optional_helpers =
   [(["c_COMBI", "c_COMBK"], @{thms COMBI_def COMBK_def}),
    (["c_COMBB", "c_COMBC"], @{thms COMBB_def COMBC_def}),

     fun aux (AQuant (q, xs, phi)) = AQuant (q, xs, aux phi)
       | aux (AConn (c, phis)) = AConn (c, map aux phis)
       | aux (AAtom tm) = AAtom (fo_term_for_combterm full_types tm)
   in aux end
 
-fun formula_for_axiom full_types (FOLFormula {combformula, ctypes_sorts, ...}) =
+fun formula_for_axiom full_types
+                      ({combformula, ctypes_sorts, ...} : fol_formula) =
   mk_ahorn (map (formula_for_fo_literal o fo_literal_for_type_literal)
                 (type_literals_for_types ctypes_sorts))
            (formula_for_combformula full_types combformula)
 
-fun problem_line_for_fact prefix full_types
-                          (formula as FOLFormula {name, kind, ...}) =
+fun problem_line_for_fact prefix full_types (formula as {name, kind, ...}) =
   Fof (prefix ^ ascii_of name, kind, formula_for_axiom full_types formula)
 
 fun problem_line_for_class_rel_clause (ClassRelClause {name, subclass,
                                                        superclass, ...}) =
   let val ty_arg = ATerm (("T", "T"), []) in

                       o fo_literal_for_arity_literal) premLits)
                 (formula_for_fo_literal
                      (fo_literal_for_arity_literal conclLit)))
 
 fun problem_line_for_conjecture full_types
-                                (FOLFormula {name, kind, combformula, ...}) =
+                                ({name, kind, combformula, ...} : fol_formula) =
   Fof (conjecture_prefix ^ name, kind,
        formula_for_combformula full_types combformula)
 
-fun free_type_literals_for_conjecture (FOLFormula {ctypes_sorts, ...}) =
+fun free_type_literals_for_conjecture ({ctypes_sorts, ...} : fol_formula) =
   map fo_literal_for_type_literal (type_literals_for_types ctypes_sorts)
 
 fun problem_line_for_free_type lit =
   Fof (tfrees_name, Hypothesis, formula_for_fo_literal lit)
 fun problem_lines_for_free_types conjectures =