subalgebra: drop arities if desired
authorhaftmann
Sun Feb 22 18:00:05 2009 +0100 (2009-02-22)
changeset 30060672012330c4e
parent 30059 c53242ef274e
child 30061 c95e8f696b68
subalgebra: drop arities if desired
src/Pure/Isar/code.ML
src/Pure/sorts.ML
     1.1 --- a/src/Pure/Isar/code.ML	Sun Feb 22 17:33:16 2009 +0100
     1.2 +++ b/src/Pure/Isar/code.ML	Sun Feb 22 18:00:05 2009 +0100
     1.3 @@ -489,7 +489,7 @@
     1.4  
     1.5  fun retrieve_algebra thy operational =
     1.6    Sorts.subalgebra (Syntax.pp_global thy) operational
     1.7 -    (arity_constraints thy (Sign.classes_of thy))
     1.8 +    (SOME o arity_constraints thy (Sign.classes_of thy))
     1.9      (Sign.classes_of thy);
    1.10  
    1.11  in
     2.1 --- a/src/Pure/sorts.ML	Sun Feb 22 17:33:16 2009 +0100
     2.2 +++ b/src/Pure/sorts.ML	Sun Feb 22 18:00:05 2009 +0100
     2.3 @@ -48,7 +48,7 @@
     2.4    val merge_algebra: Pretty.pp -> algebra * algebra -> algebra
     2.5    val classrels_of: algebra -> (class * class list) list
     2.6    val instances_of: algebra -> (string * class) list
     2.7 -  val subalgebra: Pretty.pp -> (class -> bool) -> (class * string -> sort list)
     2.8 +  val subalgebra: Pretty.pp -> (class -> bool) -> (class * string -> sort list option)
     2.9      -> algebra -> (sort -> sort) * algebra
    2.10    type class_error
    2.11    val class_error: Pretty.pp -> class_error -> string
    2.12 @@ -322,8 +322,8 @@
    2.13    let
    2.14      val restrict_sort = minimize_sort algebra o filter P o Graph.all_succs classes;
    2.15      fun restrict_arity tyco (c, (_, Ss)) =
    2.16 -      if P c then
    2.17 -        SOME (c, (c, Ss |> map2 (curry (inter_sort algebra)) (sargs (c, tyco))
    2.18 +      if P c then case sargs (c, tyco)
    2.19 +       of SOME sorts => SOME (c, (c, Ss |> map2 (curry (inter_sort algebra)) sorts
    2.20            |> map restrict_sort))
    2.21        else NONE;
    2.22      val classes' = classes |> Graph.subgraph P;