diff -r 65bdcc42badd -r 2725853f43b9 Nominal/Ex/ExCoreHaskell.thy --- a/Nominal/Ex/ExCoreHaskell.thy Tue May 04 17:25:58 2010 +0200 +++ b/Nominal/Ex/ExCoreHaskell.thy Wed May 05 10:24:54 2010 +0100 @@ -658,7 +658,7 @@ (* for the moment, we force it to be *) (*declare permute_pure[eqvt]*) -(*setup {* Context.theory_map (Nominal_ThmDecls.add_thm @{thm "permute_pure"}) *} +(*setup {* Context.theory_map (Nominal_ThmDecls.add_thm @{thm "permute_pure"}) *) thm eqvts thm eqvts_raw @@ -669,7 +669,7 @@ equivariance alpha_tkind_raw thm eqvts -thm eqvts_raw*) +thm eqvts_raw end