# HG changeset patch
# User huffman
# Date 1269294277 25200
# Node ID 0b43ff2d2e9112a252443b33573f34ec03d80917
# Parent  81608655c69ec0fa2e6abd7ed240d53e99700530
fix ML warnings in fixrec.ML

diff -r 81608655c69e -r 0b43ff2d2e91 src/HOLCF/Tools/fixrec.ML
--- a/src/HOLCF/Tools/fixrec.ML	Mon Mar 22 14:11:13 2010 -0700
+++ b/src/HOLCF/Tools/fixrec.ML	Mon Mar 22 14:44:37 2010 -0700
@@ -275,12 +275,16 @@
 (* this is the pattern-matching compiler function *)
 fun compile_pats match_name eqs =
   let
-    val (((n::names),(a::arities)),mats) =
+    val ((names, arities), mats) =
       apfst ListPair.unzip (ListPair.unzip (map (match_eq match_name) eqs));
-    val cname = if forall (fn x => n=x) names then n
-          else fixrec_err "all equations in block must define the same function";
-    val arity = if forall (fn x => a=x) arities then a
-          else fixrec_err "all equations in block must have the same arity";
+    val cname =
+        case distinct (op =) names of
+          [n] => n
+        | _ => fixrec_err "all equations in block must define the same function";
+    val arity =
+        case distinct (op =) arities of
+          [a] => a
+        | _ => fixrec_err "all equations in block must have the same arity";
     val rhs = fatbar arity mats;
   in
     mk_trp (cname === rhs)
@@ -311,7 +315,8 @@
       else HOLogic.dest_Trueprop (Logic.strip_imp_concl t);
     fun tac (t, i) =
       let
-        val Const (c, T) = head_of (chead_of (fst (HOLogic.dest_eq (concl t))));
+        val (c, T) =
+            (dest_Const o head_of o chead_of o fst o HOLogic.dest_eq o concl) t;
         val unfold_thm = the (Symtab.lookup tab c);
         val rule = unfold_thm RS @{thm ssubst_lhs};
       in