--- a/Nominal/NewParser.thy	Sun Aug 29 01:17:36 2010 +0800
+++ b/Nominal/NewParser.thy	Sun Aug 29 01:45:07 2010 +0800
@@ -540,18 +540,23 @@
       ||>> lift_thms qtys [] raw_exhaust_thms
     else raise TEST lthyA
 
-  (* Supports lemmas *) 
-
+  (* supports lemmas *) 
   val qsupports_thms =
     if get_STEPS lthy > 28
     then prove_supports lthyB qperm_simps qtrms
     else raise TEST lthyB
 
+  (* finite supp lemmas *)
   val qfsupp_thms =
     if get_STEPS lthy > 29
     then prove_fsupp lthyB qtys qinduct qsupports_thms
     else raise TEST lthyB
 
+  (* fs instances *)
+  val lthyC =
+    if get_STEPS lthy > 30
+    then fs_instance qtys qty_full_names tvs qfsupp_thms lthyB
+    else raise TEST lthyB
 
   (* noting the theorems *)  
 
@@ -560,7 +565,7 @@
     the_default (Binding.name (space_implode "_" qty_names)) opt_thms_name 
   fun thms_suffix s = Binding.qualified true s thms_name 
 
-  val (_, lthy9') = lthyB
+  val (_, lthy9') = lthyC
      |> Local_Theory.note ((thms_suffix "distinct", []), qdistincts) 
      ||>> Local_Theory.note ((thms_suffix "eq_iff", []), qeq_iffs)
      ||>> Local_Theory.note ((thms_suffix "fv_defs", []), qfv_defs)