# HG changeset patch
# User wenzelm
# Date 1427148753 -3600
# Node ID d9765e17947f144f2cd21895ab4ebb19b1946933
# Parent  85c572d089fc40eccaf9274730b91e855c47f8d3
tuned proof;

diff -r 85c572d089fc -r d9765e17947f src/HOL/HOLCF/Compact_Basis.thy
--- a/src/HOL/HOLCF/Compact_Basis.thy	Mon Mar 23 22:57:04 2015 +0100
+++ b/src/HOL/HOLCF/Compact_Basis.thy	Mon Mar 23 23:12:33 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="{arbitrary}" in exI)
+  apply (rule_tac x="{a}" for a in exI)
   apply simp
   done