src/Pure/axclass.ML
changeset 27497 c683836fe908
parent 27397 1d8456c5d53d
child 27547 13199740ced6
     1.1 --- a/src/Pure/axclass.ML	Tue Jul 08 18:13:09 2008 +0200
     1.2 +++ b/src/Pure/axclass.ML	Tue Jul 08 18:13:10 2008 +0200
     1.3 @@ -37,7 +37,7 @@
     1.4    val unoverload_const: theory -> string * typ -> string
     1.5    val param_of_inst: theory -> string * string -> string
     1.6    val inst_of_param: theory -> string -> (string * string) option
     1.7 -  val these_arity_tags: theory -> class * string -> Markup.property list
     1.8 +  val arity_property: theory -> class * string -> string -> string list
     1.9    type cache
    1.10    val of_sort: theory -> typ * sort -> cache -> thm list * cache  (*exception Sorts.CLASS_ERROR*)
    1.11    val cache: cache
    1.12 @@ -181,10 +181,11 @@
    1.13    | NONE => error ("Unproven type arity " ^
    1.14        Syntax.string_of_arity (ProofContext.init thy) (a, Ss, [c])));
    1.15  
    1.16 -fun these_arity_tags thy (c, a) = case find_first (fn ((c', _), _) => c = c')
    1.17 -  (these (Symtab.lookup (snd (get_instances thy)) a)) of
    1.18 -    SOME ((_, _), th) => Thm.get_tags th
    1.19 -  | NONE => [];
    1.20 +fun arity_property thy (c, a) x =
    1.21 +  these (Symtab.lookup (snd (get_instances thy)) a)
    1.22 +  |> map_filter (fn ((c', _), th) => if c = c'
    1.23 +        then AList.lookup (op =) (Thm.get_tags th) x else NONE)
    1.24 +  |> rev;
    1.25  
    1.26  fun put_arity ((t, Ss, c), th) = map_instances (fn (classrel, arities) =>
    1.27    (classrel, arities |> Symtab.insert_list (eq_fst op =) (t, ((c, Ss), th))));