# HG changeset patch
# User ballarin
# Date 1191234285 -7200
# Node ID f0dba1cda0b58457eef4ae1b600eb638b4bb433d
# Parent  df56433cc05997c61e0ab868ddea228a37f7abdc
unfold_locales workaround

diff -r df56433cc059 -r f0dba1cda0b5 src/FOL/ex/LocaleTest.thy
--- a/src/FOL/ex/LocaleTest.thy	Mon Oct 01 12:24:07 2007 +0200
+++ b/src/FOL/ex/LocaleTest.thy	Mon Oct 01 12:24:45 2007 +0200
@@ -209,6 +209,7 @@
   interpret i9: ID [a beta _]
     apply - apply assumption
     apply unfold_locales
+    apply (rule refl) (*FIXME: should have been discharged by unfold_locales*)
     apply (rule refl) done
 qed rule