# 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,