src/HOL/Tools/res_clause.ML
changeset 19642 ea7162f84677
parent 19521 cfdab6a91332
child 19719 837025cc6317
     1.1 --- a/src/HOL/Tools/res_clause.ML	Tue May 16 13:01:23 2006 +0200
     1.2 +++ b/src/HOL/Tools/res_clause.ML	Tue May 16 13:01:24 2006 +0200
     1.3 @@ -689,12 +689,8 @@
     1.4  
     1.5  fun classrelClauses_of (sub,sups) = classrelClauses_of_aux 0 sub sups;
     1.6  
     1.7 -val classrel_of = #2 o #classes o Type.rep_tsig o Sign.tsig_of;
     1.8 -
     1.9 -fun classrel_clauses_classrel (C: Sorts.classes) =
    1.10 -  map classrelClauses_of (Graph.dest C);
    1.11 -
    1.12 -val classrel_clauses_thy = List.concat o classrel_clauses_classrel o classrel_of;
    1.13 +val classrel_clauses_thy =
    1.14 +  maps classrelClauses_of o Graph.dest o #classes o Sorts.rep_algebra o Sign.classes_of;
    1.15  
    1.16  
    1.17  (** Isabelle arities **)
    1.18 @@ -713,8 +709,9 @@
    1.19        multi_arity_clause tc_arlists 
    1.20  
    1.21  fun arity_clause_thy thy =
    1.22 -  let val arities =
    1.23 -    Symtab.dest (Sign.arities_of thy) |> map (apsnd (map (fn (c, (_, Ss)) => (c, Ss))));
    1.24 +  let val arities = thy |> Sign.classes_of
    1.25 +    |> Sorts.rep_algebra |> #arities |> Symtab.dest
    1.26 +    |> map (apsnd (map (fn (c, (_, Ss)) => (c, Ss))));
    1.27    in multi_arity_clause (rev arities) end;
    1.28  
    1.29