diff -r 6b496f69f76c -r a27215ab674e Nominal/nominal_dt_alpha.ML
--- a/Nominal/nominal_dt_alpha.ML	Tue Jun 28 14:45:30 2011 +0900
+++ b/Nominal/nominal_dt_alpha.ML	Wed Jun 29 00:48:50 2011 +0100
@@ -13,10 +13,10 @@
     bclause list list list -> term list -> Proof.context -> 
     term list * term list * thm list * thm list * thm * local_theory
 
-  val mk_alpha_distincts: Proof.context -> thm list -> thm list -> 
+  val raw_prove_alpha_distincts: Proof.context -> thm list -> thm list -> 
     term list -> string list -> thm list
 
-  val mk_alpha_eq_iff: Proof.context -> thm list -> thm list -> thm list -> 
+  val raw_prove_alpha_eq_iff: Proof.context -> thm list -> thm list -> thm list -> 
     thm list -> thm list
 
   val induct_prove: typ list -> (typ * (term -> term)) list -> thm -> 
@@ -297,7 +297,7 @@
   THEN_ALL_NEW asm_full_simp_tac (HOL_ss addsimps distinct_thms)
 
 
-fun mk_alpha_distincts ctxt cases_thms distinct_thms alpha_trms alpha_str =
+fun raw_prove_alpha_distincts ctxt cases_thms distinct_thms alpha_trms alpha_str =
   let
     val ty_trm_assoc = alpha_str ~~ (map (fst o dest_Const) alpha_trms)
 
@@ -341,7 +341,7 @@
     else HOLogic.mk_Trueprop (HOLogic.mk_eq (concl, list_conj hyps))
   end;
 
-fun mk_alpha_eq_iff ctxt alpha_intros distinct_thms inject_thms alpha_elims =
+fun raw_prove_alpha_eq_iff ctxt alpha_intros distinct_thms inject_thms alpha_elims =
   let
     val ((_, thms_imp), ctxt') = Variable.import false alpha_intros ctxt;
     val goals = map mk_alpha_eq_iff_goal thms_imp;