1.1 --- a/src/HOL/Tools/ATP/atp_translate.ML Tue Jun 21 17:17:39 2011 +0200
1.2 +++ b/src/HOL/Tools/ATP/atp_translate.ML Tue Jun 21 17:17:39 2011 +0200
1.3 @@ -417,15 +417,19 @@
1.4 end
1.5
1.6 fun arity_clause _ _ (_, []) = []
1.7 - | arity_clause seen n (tcons, ("HOL.type",_)::ars) = (*ignore*)
1.8 - arity_clause seen n (tcons,ars)
1.9 - | arity_clause seen n (tcons, (ar as (class,_)) :: ars) =
1.10 - if member (op =) seen class then (*multiple arities for the same tycon, class pair*)
1.11 - make_axiom_arity_clause (tcons, lookup_const tcons ^ "_" ^ class ^ "_" ^ string_of_int n, ar) ::
1.12 - arity_clause seen (n+1) (tcons,ars)
1.13 - else
1.14 - make_axiom_arity_clause (tcons, lookup_const tcons ^ "_" ^ class, ar) ::
1.15 - arity_clause (class::seen) n (tcons,ars)
1.16 + | arity_clause seen n (tcons, ("HOL.type", _) :: ars) = (* ignore *)
1.17 + arity_clause seen n (tcons, ars)
1.18 + | arity_clause seen n (tcons, (ar as (class, _)) :: ars) =
1.19 + if member (op =) seen class then
1.20 + (* multiple arities for the same (tycon, class) pair *)
1.21 + make_axiom_arity_clause (tcons,
1.22 + lookup_const tcons ^ "___" ^ ascii_of class ^ "_" ^ string_of_int n,
1.23 + ar) ::
1.24 + arity_clause seen (n + 1) (tcons, ars)
1.25 + else
1.26 + make_axiom_arity_clause (tcons, lookup_const tcons ^ "___" ^
1.27 + ascii_of class, ar) ::
1.28 + arity_clause (class :: seen) n (tcons, ars)
1.29
1.30 fun multi_arity_clause [] = []
1.31 | multi_arity_clause ((tcons, ars) :: tc_arlists) =
1.32 @@ -1592,7 +1596,7 @@
1.33
1.34 fun formula_line_for_arity_clause ({name, prem_lits, concl_lits, ...}
1.35 : arity_clause) =
1.36 - Formula (arity_clause_prefix ^ ascii_of name, Axiom,
1.37 + Formula (arity_clause_prefix ^ name, Axiom,
1.38 mk_ahorn (map (formula_from_fo_literal o apfst not
1.39 o fo_literal_from_arity_literal) prem_lits)
1.40 (formula_from_fo_literal