# HG changeset patch # User paulson # Date 1164110139 -3600 # Node ID 625797c592b2ccb4705511a49c866a2d9beb4efd # Parent ef9080e7dbbc8b08a83647aac35af18cf70d5396 Optimized class_pairs for the common case of no subclasses diff -r ef9080e7dbbc -r 625797c592b2 src/HOL/Tools/res_clause.ML --- a/src/HOL/Tools/res_clause.ML Tue Nov 21 12:51:20 2006 +0100 +++ b/src/HOL/Tools/res_clause.ML Tue Nov 21 12:55:39 2006 +0100 @@ -529,12 +529,13 @@ superclass: class}; (*Generate all pairs (sub,super) such that sub is a proper subclass of super in theory thy.*) -fun class_pairs thy subs supers = - let val class_less = Sorts.class_less(Sign.classes_of thy) - fun add_super sub (super,pairs) = - if class_less (sub,super) then (sub,super)::pairs else pairs - fun add_supers (sub,pairs) = foldl (add_super sub) pairs supers - in foldl add_supers [] subs end; +fun class_pairs thy [] supers = [] + | class_pairs thy subs supers = + let val class_less = Sorts.class_less(Sign.classes_of thy) + fun add_super sub (super,pairs) = + if class_less (sub,super) then (sub,super)::pairs else pairs + fun add_supers (sub,pairs) = foldl (add_super sub) pairs supers + in foldl add_supers [] subs end; fun make_classrelClause (sub,super) = ClassrelClause {axiom_name = clrelclause_prefix ^ ascii_of sub ^ "_" ^ ascii_of super,