# HG changeset patch
# User wenzelm
# Date 1180905405 -7200
# Node ID 8eac3bda1063d060dc8eaf067eb8328efbac38e5
# Parent  49c78d67b807d1ac9a799615c07f34ab7b2335f7
name_of_fqgar: precise type;

diff -r 49c78d67b807 -r 8eac3bda1063 src/HOL/Tools/function_package/mutual.ML
--- 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 *)