--- a/Nominal/nominal_function_core.ML	Tue Jan 25 02:51:44 2011 +0900
+++ b/Nominal/nominal_function_core.ML	Tue Jan 25 18:58:26 2011 +0100
@@ -115,6 +115,14 @@
     |> HOLogic.mk_Trueprop
   end
 
+fun mk_eqvt trm =
+  let
+    val ty = fastype_of trm
+  in
+    Const (@{const_name eqvt}, ty --> @{typ bool}) $ trm
+    |> HOLogic.mk_Trueprop
+  end
+
 (* nominal *)
 fun find_calls2 f t = 
   let
@@ -496,18 +504,19 @@
       |> (fn it => Drule.compose_single (it, 2, acc_induct_rule)) (* "EX! y. (?x,y):G" *)
       |> (fn it => fold (Thm.forall_intr o cterm_of thy o Var) (Term.add_vars (prop_of it) []) it)
 
-    val goalstate =  Conjunction.intr graph_is_function complete
+    val goalstate =  
+         Conjunction.intr (Conjunction.intr graph_is_function complete) G_eqvt 
       |> Thm.close_derivation
       |> Goal.protect
       |> fold_rev (Thm.implies_intr o cprop_of) compat
       |> Thm.implies_intr (cprop_of complete)
+      |> Thm.implies_intr (cprop_of G_eqvt)
   in
     (goalstate, values)
   end
 
-(* nominal *) 
 (* wrapper -- restores quantifiers in rule specifications *)
-fun inductive_def eqvt_flag (binding as ((R, T), _)) intrs lthy =
+fun inductive_def (binding as ((R, T), _)) intrs lthy =
   let
     val ({intrs = intrs_gen, elims = [elim_gen], preds = [ Rdef ], induct, raw_induct, ...}, lthy) =
       lthy
@@ -527,16 +536,6 @@
           [] (* no special monos *)
       ||> Local_Theory.restore_naming lthy
 
-    val eqvt_thm' = 
-      if eqvt_flag = false then NONE
-      else 
-        let
-          (* val _ = tracing ("intrs:\n" ^ cat_lines (map @{make_string} intrs_gen)) *)
-          val ([eqvt_thm], lthy) = Nominal_Eqvt.raw_equivariance false [Rdef] raw_induct intrs_gen lthy
-        in
-          SOME ((Nominal_ThmDecls.eqvt_transform lthy eqvt_thm) RS @{thm eqvtI})
-        end
-
     val cert = cterm_of (ProofContext.theory_of lthy)
     fun requantify orig_intro thm =
       let
@@ -550,7 +549,7 @@
           forall_intr_rename (n, cert (Var (varmap (n, T), T)))) qs thm
       end
   in
-    ((Rdef, map2 requantify intrs intrs_gen, forall_intr_vars elim_gen, induct, eqvt_thm'), lthy)
+    ((Rdef, map2 requantify intrs intrs_gen, forall_intr_vars elim_gen, induct), lthy)
   end
 
 (* nominal *)
@@ -574,7 +573,7 @@
 
     val G_intros = map2 mk_GIntro clauses RCss
   in
-    inductive_def true ((Binding.name n, T), NoSyn) G_intros lthy
+    inductive_def ((Binding.name n, T), NoSyn) G_intros lthy
   end
 
 fun define_function fdefname (fname, mixfix) domT ranT G default lthy =
@@ -605,8 +604,8 @@
 
     val R_intross = map2 (map o mk_RIntro) (clauses ~~ qglrs) RCss
 
-    val ((R, RIntro_thms, R_elim, _, _), lthy) =
-      inductive_def false ((Binding.name n, T), NoSyn) (flat R_intross) lthy
+    val ((R, RIntro_thms, R_elim, _), lthy) =
+      inductive_def ((Binding.name n, T), NoSyn) (flat R_intross) lthy
   in
     ((R, Library.unflat R_intross RIntro_thms, R_elim), lthy)
   end
@@ -988,7 +987,7 @@
     val trees = map build_tree clauses
     val RCss = map find_calls trees
 
-    val ((G, GIntro_thms, G_elim, G_induct, SOME G_eqvt), lthy) =
+    val ((G, GIntro_thms, G_elim, G_induct), lthy) =
       PROFILE "def_graph" (define_graph (graph_name defname) fvar domT ranT clauses RCss) lthy
 
     val ((f, (_, f_defthm)), lthy) =
@@ -1019,6 +1018,8 @@
       mk_compat_proof_obligations domT ranT fvar f abstract_qglrs 
       |> map (cert #> Thm.assume)
 
+    val G_eqvt = mk_eqvt G |> cert |> Thm.assume
+ 
     val compat_store = store_compat_thms n compat
 
     val (goalstate, values) = PROFILE "prove_stuff"
@@ -1032,10 +1033,11 @@
       let
         val newthy = theory_of_thm provedgoal (*FIXME*)
 
-        val (graph_is_function, complete_thm) =
+        val ((graph_is_function, complete_thm), _) =
           provedgoal
           |> Conjunction.elim
-          |> apfst (Thm.forall_elim_vars 0)
+          |>> Conjunction.elim
+          |>> apfst (Thm.forall_elim_vars 0)
 
         val f_iff = graph_is_function RS (f_defthm RS ex1_implies_iff)