--- a/src/HOL/Tools/function_package/mutual.ML Sun Jun 03 23:16:44 2007 +0200
+++ b/src/HOL/Tools/function_package/mutual.ML Sun Jun 03 23:16:45 2007 +0200
@@ -34,7 +34,7 @@
type qgar = string * (string * typ) list * term list * term list * term
-fun name_of_fqgar (f, _, _, _, _) = f
+fun name_of_fqgar ((f, _, _, _, _): qgar) = f
datatype mutual_part =
MutualPart of
@@ -302,7 +302,7 @@
if P (x, l) then ((l, x::xs)::bs) else ((l, xs)::store_grouped P x bs)
fun sort_by_function (Mutual {fqgars, ...}) names xs =
- fold_rev (store_grouped (eq_str o apfst fst)) (* fill *)
+ fold_rev (store_grouped (op = o apfst fst)) (* fill *)
(map name_of_fqgar (Library.take (length xs, fqgars)) ~~ xs) (* the name-thm pairs *)
(map (rpair []) names) (* in the empty buckets labeled with names *)