# HG changeset patch
# User haftmann
# Date 1235320396 -3600
# Node ID c53242ef274ed2b97882f033e05e2f30c29e084c
# Parent  f84c2412e87056941cca8bb2a14f29277d3dd9fc# Parent  bf6b35c5c0fc9c736a9912683feae63157ded443
merged

diff -r bf6b35c5c0fc -r c53242ef274e src/Tools/code/code_wellsorted.ML
--- a/src/Tools/code/code_wellsorted.ML	Sun Feb 22 17:25:45 2009 +0100
+++ b/src/Tools/code/code_wellsorted.ML	Sun Feb 22 17:33:16 2009 +0100
@@ -99,7 +99,7 @@
 
 fun obtain_eqns thy eqngr c =
   case try (Graph.get_node eqngr) c
-   of SOME ((lhs, _), eqns) => ((lhs, []), eqns)
+   of SOME ((lhs, _), eqns) => ((lhs, []), [])
     | NONE => let
         val eqns = Code.these_eqns thy c
           |> burrow_fst (Code_Unit.norm_args thy)
@@ -223,9 +223,10 @@
       |> map swap (*FIXME*)
     fun add_class (class, superclasses) algebra =
       Sorts.add_class pp (class, Sorts.minimize_sort algebra superclasses) algebra;
-    fun add_arity (class, tyco) algebra = Sorts.add_arities pp
-      (tyco, [(class, ((map (Sorts.minimize_sort algebra) o the
-        o AList.lookup (op =) arities) (class, tyco)))]) algebra;
+    fun add_arity (class, tyco) algebra = case AList.lookup (op =) arities (class, tyco)
+     of SOME sorts => Sorts.add_arities pp
+         (tyco, [(class, map (Sorts.minimize_sort algebra) sorts)]) algebra
+      | NONE => algebra;
   in
     Sorts.empty_algebra
     |> fold add_class classrels
@@ -247,13 +248,14 @@
   end;
 
 fun add_arity thy vardeps (class, tyco) =
-  AList.update (op =)
+  AList.default (op =)
     ((class, tyco), map (fn k => (snd o Vargraph.get_node vardeps) (Inst (class, tyco), k))
       (0 upto Sign.arity_number thy tyco - 1));
 
 fun add_eqs thy (proj_sort, algebra) vardeps
     (c, (proto_lhs, proto_eqns)) (rhss, eqngr) =
-  let
+  if can (Graph.get_node eqngr) c then (rhss, eqngr)
+  else let
     val lhs = map_index (fn (k, (v, _)) =>
       (v, snd (Vargraph.get_node vardeps (Fun c, k)))) proto_lhs;
     val inst_tab = Vartab.empty |> fold (fn (v, sort) =>