# HG changeset patch
# User wenzelm
# Date 1427210208 -3600
# Node ID f313ca9fbba0ab7947b0499d7bf27070ce8deaec
# Parent  f05ef8c62e4f3b8b13612c5b56000870e9185546
tuned proof;

diff -r f05ef8c62e4f -r f313ca9fbba0 src/HOL/HOLCF/Compact_Basis.thy
--- a/src/HOL/HOLCF/Compact_Basis.thy	Tue Mar 24 15:57:51 2015 +0100
+++ b/src/HOL/HOLCF/Compact_Basis.thy	Tue Mar 24 16:16:48 2015 +0100
@@ -16,7 +16,7 @@
 
 typedef 'a pd_basis = "pd_basis :: 'a compact_basis set set"
   unfolding pd_basis_def
-  apply (rule_tac x="{a}" for a in exI)
+  apply (rule_tac x="{_}" in exI)
   apply simp
   done