src/HOL/Tools/res_clause.ML
changeset 21432 625797c592b2
parent 21416 f23e4e75dfd3
child 21470 7c1b59ddcd56
     1.1 --- a/src/HOL/Tools/res_clause.ML	Tue Nov 21 12:51:20 2006 +0100
     1.2 +++ b/src/HOL/Tools/res_clause.ML	Tue Nov 21 12:55:39 2006 +0100
     1.3 @@ -529,12 +529,13 @@
     1.4  			    superclass: class};
     1.5   
     1.6  (*Generate all pairs (sub,super) such that sub is a proper subclass of super in theory thy.*)
     1.7 -fun class_pairs thy subs supers =
     1.8 -  let val class_less = Sorts.class_less(Sign.classes_of thy)
     1.9 -      fun add_super sub (super,pairs) = 
    1.10 -            if class_less (sub,super) then (sub,super)::pairs else pairs
    1.11 -      fun add_supers (sub,pairs) = foldl (add_super sub) pairs supers
    1.12 -  in  foldl add_supers [] subs  end;
    1.13 +fun class_pairs thy [] supers = []
    1.14 +  | class_pairs thy subs supers =
    1.15 +      let val class_less = Sorts.class_less(Sign.classes_of thy)
    1.16 +	  fun add_super sub (super,pairs) = 
    1.17 +		if class_less (sub,super) then (sub,super)::pairs else pairs
    1.18 +	  fun add_supers (sub,pairs) = foldl (add_super sub) pairs supers
    1.19 +      in  foldl add_supers [] subs  end;
    1.20  
    1.21  fun make_classrelClause (sub,super) =
    1.22    ClassrelClause {axiom_name = clrelclause_prefix ^ ascii_of sub ^ "_" ^ ascii_of super,