--- a/Nominal/Manual/Term4.thy	Thu Apr 15 13:55:44 2010 +0200
+++ b/Nominal/Manual/Term4.thy	Thu Apr 15 14:08:08 2010 +0200
@@ -73,9 +73,10 @@
 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha4_reflp}, []),
   build_alpha_refl [((0, @{term alpha_rtrm4}), 0), ((0, @{term alpha_rtrm4_list}), 0)] [@{term alpha_rtrm4}, @{term alpha_rtrm4_list}] @{thm rtrm4.induct} @{thms alpha4_inj_no} ctxt) ctxt)) *}
 thm alpha4_reflp
+ML build_equivps
 
 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha4_equivp_no}, []),
-  (build_equivps [@{term alpha_rtrm4}, @{term alpha_rtrm4_list}] @{thm rtrm4.induct} @{thm alpha_rtrm4_alpha_rtrm4_list.induct} @{thms rtrm4.inject list.inject} @{thms alpha4_inj_no} @{thms rtrm4.distinct list.distinct} @{thms alpha_rtrm4_list.cases alpha_rtrm4.cases} @{thms alpha4_eqvt_no} ctxt)) ctxt)) *}
+  (build_equivps [@{term alpha_rtrm4}, @{term alpha_rtrm4_list}] @{thms alpha4_reflp} @{thm alpha_rtrm4_alpha_rtrm4_list.induct} @{thms rtrm4.inject list.inject} @{thms alpha4_inj_no} @{thms rtrm4.distinct list.distinct} @{thms alpha_rtrm4_list.cases alpha_rtrm4.cases} @{thms alpha4_eqvt_no} ctxt)) ctxt)) *}
 lemmas alpha4_equivp = alpha4_equivp_no[simplified fix2]
 
 (*lemma fv_rtrm4_rsp:
@@ -94,9 +95,9 @@
 
 local_setup {*
 (fn ctxt => ctxt
- |> snd o (Quotient_Def.quotient_lift_const ("Vr4", @{term rVr4}))
- |> snd o (Quotient_Def.quotient_lift_const ("Ap4", @{term rAp4}))
- |> snd o (Quotient_Def.quotient_lift_const ("Lm4", @{term rLm4})))
+ |> snd o (Quotient_Def.quotient_lift_const [] ("Vr4", @{term rVr4}))
+ |> snd o (Quotient_Def.quotient_lift_const [] ("Ap4", @{term rAp4}))
+ |> snd o (Quotient_Def.quotient_lift_const [] ("Lm4", @{term rLm4})))
 *}
 print_theorems