diff -r 6e37bfb62474 -r 486d4647bb37 Nominal/Nominal2.thy
--- a/Nominal/Nominal2.thy	Sun Sep 05 07:00:19 2010 +0800
+++ b/Nominal/Nominal2.thy	Fri Sep 10 09:17:40 2010 +0800
@@ -249,7 +249,6 @@
 end
 *}
 
-
 ML {*
 (* for testing porposes - to exit the procedure early *)
 exception TEST of Proof.context
@@ -259,6 +258,7 @@
 fun get_STEPS ctxt = Config.get ctxt STEPS
 *}
 
+
 setup STEPS_setup
 
 ML {*
@@ -333,9 +333,8 @@
     mk_alpha_distincts lthy4 alpha_cases raw_distinct_thms alpha_trms raw_tys
 
   (* definition of alpha_eq_iff  lemmas *)
-  (* they have a funny shape for the simplifier ---- CHECK WHETHER NEEDED*)
   val _ = warning "Eq-iff theorems";
-  val (alpha_eq_iff_simps, alpha_eq_iff) = 
+  val alpha_eq_iff = 
     if get_STEPS lthy > 5
     then mk_alpha_eq_iff lthy4 alpha_intros raw_distinct_thms raw_inject_thms alpha_cases
     else raise TEST lthy4
@@ -542,6 +541,7 @@
   val qinducts = Project_Rule.projections lthyA qinduct
 
   (* supports lemmas *) 
+  val _ = warning "Proving Supports Lemmas and fs-Instances"
   val qsupports_thms =
     if get_STEPS lthy > 28
     then prove_supports lthyB qperm_simps qtrms
@@ -559,6 +559,15 @@
     then fs_instance qtys qty_full_names tvs qfsupp_thms lthyB
     else raise TEST lthyB
 
+  (* fv - supp equality *)
+  val _ = warning "Proving Equality between fv and supp"
+  val qfv_supp_thms = 
+    if get_STEPS lthy > 31
+    then prove_fv_supp qtys qfvs qfv_bns qalpha_bns qbn_defs qfv_defs qeq_iffs 
+      qperm_simps qfv_qbn_eqvts qinducts (flat raw_bclauses) lthyC
+    else []
+
+ 
   (* noting the theorems *)  
 
   (* generating the prefix for the theorem names *)
@@ -575,15 +584,17 @@
      ||>> Local_Theory.note ((thms_suffix "fv_bn_eqvt", []), qfv_qbn_eqvts) 
      ||>> Local_Theory.note ((thms_suffix "size_eqvt", []), qsize_eqvt)
      ||>> Local_Theory.note ((thms_suffix "induct", []), [qinduct]) 
-     ||>> Local_Theory.note ((thms_suffix "inducts", []), qinducts) 
+     ||>> Local_Theory.note ((thms_suffix "inducts", []), qinducts)
      ||>> Local_Theory.note ((thms_suffix "exhaust", []), qexhausts)
      ||>> Local_Theory.note ((thms_suffix "supports", []), qsupports_thms)
      ||>> Local_Theory.note ((thms_suffix "fsupp", []), qfsupp_thms)
+     ||>> Local_Theory.note ((thms_suffix "supp", []), qfv_supp_thms)
 in
   (0, lthy9')
 end handle TEST ctxt => (0, ctxt)
 *}
 
+
 section {* Preparing and parsing of the specification *}
 
 ML {*