# HG changeset patch
# User haftmann
# Date 1372446462 -7200
# Node ID 445ae7a4e4e1a3b394562ce1cb646f80ac71fd60
# Parent  9c7f760d06c2ec3dd1409493c216cc3a926c698e
sort out code equations headed by a projection of a abstract datatype

diff -r 9c7f760d06c2 -r 445ae7a4e4e1 src/Pure/Isar/code.ML
--- 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) =