# HG changeset patch
# User huffman
# Date 1210966867 -7200
# Node ID 5d9f78c3d6de3fe23b4c102c801507e219650b3c
# Parent  7f5b390a4448acfd4961d1651789f0c27f9d62ab
fix looping simplifier

diff -r 7f5b390a4448 -r 5d9f78c3d6de src/HOLCF/SetPcpo.thy
--- a/src/HOLCF/SetPcpo.thy	Thu May 15 22:57:54 2008 +0200
+++ b/src/HOLCF/SetPcpo.thy	Fri May 16 21:41:07 2008 +0200
@@ -16,7 +16,7 @@
   less_bool_def: "(op \<sqsubseteq>) = (op \<longrightarrow>)"
 
 instance
-by (intro_classes, auto simp add: less_bool_def)
+by (intro_classes, unfold less_bool_def, safe)
 
 end