# HG changeset patch
# User haftmann
# Date 1285001006 -7200
# Node ID 839a0446630b302a9f35d5603c3255baf26f1307
# Parent  5ee997fbe5cc746f2737ec2f887c563ecb3b04b2
corrected long-overlooked slip: the Pure equality of a code equation is no part of the code equation itself

diff -r 5ee997fbe5cc -r 839a0446630b src/Pure/Isar/code.ML
--- 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;