--- a/Nominal/Rsp.thy	Fri Feb 26 13:57:43 2010 +0100
+++ b/Nominal/Rsp.thy	Fri Feb 26 15:10:55 2010 +0100
@@ -69,7 +69,7 @@
    ctxt
 |> snd o Local_Theory.note 
   ((Binding.empty, [Attrib.internal (fn _ => Quotient_Info.rsp_rules_add)]), rsp_thms)
-|> snd o Local_Theory.note ((bind, []), user_thms)
+|> Local_Theory.note ((bind, []), user_thms)
 end
 *}
 
@@ -99,7 +99,7 @@
 *}
 
 (* Testing code
-local_setup {* prove_const_rsp @{binding fv_rtrm2_rsp} [@{term rbv2}]
+local_setup {* snd o prove_const_rsp @{binding fv_rtrm2_rsp} [@{term rbv2}]
   (fn _ => fv_rsp_tac @{thm alpha_rtrm2_alpha_rassign.inducts(2)} @{thms fv_rtrm2_fv_rassign.simps} 1) *}*)
 
 (*ML {*