# HG changeset patch
# User haftmann
# Date 1309554627 -7200
# Node ID f41b0d6dec99b16e5207e23cc08a41294e34f86c
# Parent  63654984ba5437b4cb4e27dd1f5e76b4825d2061
corrected misunderstanding what `old functions` are supposed to be

diff -r 63654984ba54 -r f41b0d6dec99 src/Pure/Isar/code.ML
--- a/src/Pure/Isar/code.ML	Fri Jul 01 23:07:06 2011 +0200
+++ b/src/Pure/Isar/code.ML	Fri Jul 01 23:10:27 2011 +0200
@@ -1205,7 +1205,7 @@
           (fn (c, ((_, spec), _)) =>
             if member (op =) (the_list (associated_abstype spec)) tyco
             then insert (op =) c else I)
-            ((the_functions o the_exec) thy) (old_proj :: old_constrs);
+            ((the_functions o the_exec) thy) [old_proj];
     fun drop_outdated_cases cases = fold Symtab.delete_safe
       (Symtab.fold (fn (c, ((_, (_, cos)), _)) =>
         if exists (member (op =) old_constrs) cos