sort out code equations headed by a projection of a abstract datatype

--- a/src/Pure/Isar/code.ML	Fri Jun 28 21:07:41 2013 +0200
+++ b/src/Pure/Isar/code.ML	Fri Jun 28 21:07:42 2013 +0200
@@ -502,6 +502,13 @@
     val _ = if not (is_abstr thy c) then ()
       else bad_thm "Abstractor as head in equation";
     val _ = check_decl_ty thy (c, ty);
+    val _ = case strip_type ty
+     of (Type (tyco, _) :: _, _) => (case get_type_entry thy tyco
+       of SOME (_, Abstractor (_, (proj, _))) => if c = proj
+            then bad_thm "Projection as head in equation"
+            else ()
+        | _ => ())
+      | _ => ();
   in () end;
 
 fun gen_assert_eqn thy check_patterns (thm, proper) =