corrected long-overlooked slip: the Pure equality of a code equation is no part of the code equation itself

--- a/src/Pure/Isar/code.ML	Mon Sep 20 18:43:23 2010 +0200
+++ b/src/Pure/Isar/code.ML	Mon Sep 20 18:43:26 2010 +0200
@@ -722,7 +722,8 @@
     val (args, rhs) = (apfst (snd o strip_comb) o Logic.dest_equals o subst_signatures thy) t;
     fun add_const (Const (c, ty)) = insert (op =) (c, Sign.const_typargs thy (c, ty))
       | add_const _ = I
-  in fold_aterms add_const t end;
+    val add_consts = fold_aterms add_const
+  in add_consts rhs o fold add_consts args end;
 
 fun dest_eqn thy =
   apfst (snd o strip_comb) o Logic.dest_equals o subst_signatures thy o Logic.unvarify_global;