# HG changeset patch
# User blanchet
# Date 1259943487 -3600
# Node ID 854e12dafd28d99c79cd9517d054b427377869a7
# Parent  2380c1dac86ea9f9c1d58e813b85a38abb4ed66c
make proof work again

diff -r 2380c1dac86e -r 854e12dafd28 src/HOL/Nitpick_Examples/Typedef_Nits.thy
--- a/src/HOL/Nitpick_Examples/Typedef_Nits.thy	Fri Dec 04 17:17:52 2009 +0100
+++ b/src/HOL/Nitpick_Examples/Typedef_Nits.thy	Fri Dec 04 17:18:07 2009 +0100
@@ -126,7 +126,7 @@
 
 lemma "Inl \<equiv> \<lambda>a. Abs_Sum (Inl_Rep a)"
 nitpick [card = 1, expect = none]
-by (rule Inl_def)
+by (simp only: Inl_def o_def)
 
 lemma "Inl \<equiv> \<lambda>a. Abs_Sum (Inr_Rep a)"
 nitpick [card = 1, card "'a + 'a" = 2, expect = genuine]