--- 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, _) =
--- 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