--- a/Nominal/nominal_dt_alpha.ML	Sun Sep 05 07:00:19 2010 +0800
+++ b/Nominal/nominal_dt_alpha.ML	Fri Sep 10 09:17:40 2010 +0800
@@ -14,7 +14,7 @@
     term list -> typ list -> thm list
 
   val mk_alpha_eq_iff: Proof.context -> thm list -> thm list -> thm list -> 
-    thm list -> (thm list * thm list)
+    thm list -> thm list
 
   val alpha_prove: term list -> (term * ((term * term) -> term)) list -> thm -> 
     (Proof.context -> int -> tactic) -> Proof.context -> thm list
@@ -315,11 +315,12 @@
 
 (** produces the alpha_eq_iff simplification rules **)
 
-(* in case a theorem is of the form (C.. = C..), it will be
-   rewritten to ((C.. = C..) = True) *)
+(* in case a theorem is of the form (Rel Const Const), it will be
+   rewritten to ((Rel Const = Const) = True) 
+*)
 fun mk_simp_rule thm =
   case (prop_of thm) of
-    @{term "Trueprop"} $ (Const (@{const_name "op ="}, _) $ _ $ _) => @{thm eqTrueI} OF [thm]
+    @{term "Trueprop"} $ (_ $ Const _ $ Const _) => thm RS @{thm eqTrueI}
   | _ => thm
 
 fun alpha_eq_iff_tac dist_inj intros elims =
@@ -347,7 +348,7 @@
   val thms = map (fn goal => Goal.prove ctxt' [] [] goal (K tac)) goals;
 in
   Variable.export ctxt' ctxt thms
-  |> `(map mk_simp_rule)
+  |> map mk_simp_rule
 end