| changeset 53833 | ff09afd47b34 |
| parent 53823 | 191ec7f873d5 |
| child 54061 | 6807b8e95adb |
--- a/src/HOL/Tools/monomorph.ML Tue Sep 24 19:15:49 2013 +0200 +++ b/src/HOL/Tools/monomorph.ML Tue Sep 24 19:15:50 2013 +0200 @@ -290,7 +290,7 @@ fun size_of_subst subst = Vartab.fold (Integer.add o size_of_typ o snd o snd) subst 0 -val subst_ord = int_ord o pairself size_of_subst +fun subst_ord subst = int_ord (pairself size_of_subst subst) fun instantiated_thms _ _ (Ground thm) = [(0, thm)] | instantiated_thms _ _ Ignored = []