src/HOL/HOLCF/Compact_Basis.thy
changeset 59791 d9765e17947f
parent 58880 0baae4311a9f
child 59797 f313ca9fbba0
     1.1 --- a/src/HOL/HOLCF/Compact_Basis.thy	Mon Mar 23 22:57:04 2015 +0100
     1.2 +++ b/src/HOL/HOLCF/Compact_Basis.thy	Mon Mar 23 23:12:33 2015 +0100
     1.3 @@ -16,7 +16,7 @@
     1.4  
     1.5  typedef 'a pd_basis = "pd_basis :: 'a compact_basis set set"
     1.6    unfolding pd_basis_def
     1.7 -  apply (rule_tac x="{arbitrary}" in exI)
     1.8 +  apply (rule_tac x="{a}" for a in exI)
     1.9    apply simp
    1.10    done
    1.11