--- a/Nominal/Nominal2_Abs.thy	Tue Jul 08 11:18:31 2014 +0100
+++ b/Nominal/Nominal2_Abs.thy	Thu Jul 09 02:32:46 2015 +0100
@@ -923,15 +923,15 @@
 
 ML {*
 fun alpha_single_simproc thm _ ctxt ctrm =
- let
+  let
     val thy = Proof_Context.theory_of ctxt
-    val _ $ (_ $ x) $ (_ $ y) = term_of ctrm
+    val _ $ (_ $ x) $ (_ $ y) = Thm.term_of ctrm
     val cvrs = union (op =) (Term.add_frees x []) (Term.add_frees y [])
       |> filter (fn (_, ty) => Sign.of_sort thy (ty, @{sort fs}))
       |> map Free
       |> HOLogic.mk_tuple
-      |> Thm.cterm_of thy
-    val cvrs_ty = ctyp_of_term cvrs
+      |> Thm.cterm_of ctxt
+    val cvrs_ty = Thm.ctyp_of_cterm cvrs
     val thm' = thm
       |> Drule.instantiate' [NONE, NONE, SOME cvrs_ty] [NONE, NONE, NONE, NONE, SOME cvrs] 
   in
@@ -1050,7 +1050,6 @@
 lemma [quot_respect]:
   shows "((R1 ===> op =) ===> (R2 ===> op =) ===> rel_prod R1 R2 ===> op =) prod_fv prod_fv"
   unfolding rel_fun_def
-  unfolding rel_prod_def
   by auto
 
 lemma [quot_preserve]:
@@ -1067,7 +1066,7 @@
 lemma [eqvt]: 
   shows "p \<bullet> prod_alpha A B x y = prod_alpha (p \<bullet> A) (p \<bullet> B) (p \<bullet> x) (p \<bullet> y)"
   unfolding prod_alpha_def
-  unfolding rel_prod_def
+  unfolding rel_prod_conv
   by (perm_simp) (rule refl)
 
 lemma [eqvt]: