--- a/Quot/Nominal/Fv.thy	Mon Feb 22 10:57:39 2010 +0100
+++ b/Quot/Nominal/Fv.thy	Mon Feb 22 12:12:32 2010 +0100
@@ -91,7 +91,6 @@
 *}
 
 (* TODO: Notice datatypes without bindings and replace alpha with equality *)
-
 ML {*
 (* Currently needs just one full_tname to access Datatype *)
 fun define_fv_alpha full_tname bindsall lthy =
@@ -253,4 +252,21 @@
 end
 *}
 
+ML {*
+fun build_alpha_refl_gl alphas =
+let
+  fun build_alpha alpha =
+    let
+      val ty = domain_type (fastype_of alpha);
+      val var = Free("x", ty);
+    in
+      alpha $ var $ var
+    end
+  val eqs = map build_alpha alphas
+in
+  @{term Trueprop} $ foldr1 HOLogic.mk_conj eqs
 end
+*}
+
+
+end