diff -r b355cab42841 -r 4029105011ca Nominal/Parser.thy
--- a/Nominal/Parser.thy	Thu Mar 11 16:50:44 2010 +0100
+++ b/Nominal/Parser.thy	Thu Mar 11 17:47:29 2010 +0100
@@ -283,6 +283,7 @@
 ML {* val cheat_fv_eqvt = ref true *} (* The tactic works, building the goal needs fixing *)
 ML {* val cheat_alpha_eqvt = ref true *} (* The tactic works, building the goal needs fixing *)
 
+
 ML {*
 fun nominal_datatype2 dts bn_funs bn_eqs binds lthy =
 let
@@ -304,7 +305,7 @@
   val dtinfos = map (Datatype.the_info (ProofContext.theory_of lthy2)) all_full_tnames;
   val rel_dtinfos = List.take (dtinfos, (length dts));
   val inject = flat (map #inject dtinfos);
-  val distinct = flat (map #distinct dtinfos);
+  val distincts = flat (map #distinct dtinfos);
   val rel_distinct = map #distinct rel_dtinfos;
   val induct = #induct dtinfo;
   val inducts = #inducts dtinfo;
@@ -331,7 +332,7 @@
   val alpha_intros = #intrs alpha;
   val alpha_cases_loc = #elims alpha
   val alpha_cases = ProofContext.export lthy4 lthy3 alpha_cases_loc
-  val alpha_inj_loc = build_alpha_inj alpha_intros (inject @ distinct) alpha_cases_loc lthy4
+  val alpha_inj_loc = build_alpha_inj alpha_intros (inject @ distincts) alpha_cases_loc lthy4
   val alpha_inj = ProofContext.export lthy4 lthy3 alpha_inj_loc
   fun alpha_eqvt_tac' _ =
     if !cheat_alpha_eqvt then Skip_Proof.cheat_tac thy
@@ -362,7 +363,11 @@
         Const (cname, map (typ_of_dtyp descr sorts) dts --->
           typ_of_dtyp descr sorts (DtRec i))) l) descr);
   val (consts_defs, lthy8) = fold_map Quotient_Def.quotient_lift_const (const_names ~~ raw_consts) lthy7;
-  val (consts, const_defs) = split_list consts_defs;
+  val (consts_loc, const_defs) = split_list consts_defs;
+  val morphism_8_7 = ProofContext.export_morphism lthy8 lthy7;
+  val consts = map (Morphism.term morphism_8_7) consts_loc;
+  (* Could be done nicer *)
+  val q_tys = distinct (op =) (map (snd o strip_type o fastype_of) consts);
   val (bns_rsp_pre, lthy9) = fold_map (
     fn (bn_t, i) => prove_const_rsp Binding.empty [bn_t]
       (fn _ => fvbv_rsp_tac (nth alpha_inducts i) raw_bn_eqs 1)) bns lthy8;
@@ -406,8 +411,15 @@
   val q_eqvt = map (lift_thm lthy19) raw_fv_bv_eqvt;
   val (_, lthy20) = Local_Theory.note ((Binding.empty,
     [Attrib.internal (fn _ => Nominal_ThmDecls.eqvt_add)]), q_eqvt) lthy19;
+  val supports = map (prove_supports lthy20 q_perm) consts
+  val _ = map tracing (map PolyML.makestring supports);
+  val fin_supp = HOLogic.conj_elims (prove_fs lthy20 q_induct supports q_tys);
+  val thy3 = Local_Theory.exit_global lthy20;
+  val lthy21 = Theory_Target.instantiation (qty_full_names, [], @{sort fs}) thy3;
+  fun tac _ = Class.intro_classes_tac [] THEN (ALLGOALS (resolve_tac fin_supp))
+  val lthy22 = Class.prove_instantiation_instance tac lthy21;
 in
-  ((raw_dt_names, raw_bn_funs, raw_bn_eqs, raw_binds), lthy20)
+  ((raw_dt_names, raw_bn_funs, raw_bn_eqs, raw_binds), lthy22)
 end
 *}