--- a/Nominal/nominal_function_core.ML	Mon Jul 18 10:50:21 2011 +0100
+++ b/Nominal/nominal_function_core.ML	Mon Jul 18 17:40:13 2011 +0100
@@ -19,7 +19,7 @@
     -> local_theory
     -> (term   (* f *)
         * thm  (* goalstate *)
-        * (thm -> Function_Common.function_result) (* continuation *)
+        * (thm -> Nominal_Function_Common.nominal_function_result) (* continuation *)
        ) * local_theory
 
 end
@@ -1062,6 +1062,8 @@
 
         val f_iff = graph_is_function RS (f_defthm RS ex1_implies_iff)
 
+        val f_eqvt = graph_is_function RS (G_eqvt RS (f_defthm RS @{thm fundef_ex1_eqvt}))
+
         val psimps = PROFILE "Proving simplification rules"
           (mk_psimps newthy globals R xclauses values f_iff) graph_is_function
 
@@ -1077,9 +1079,9 @@
            else NONE
 
       in
-        FunctionResult {fs=[f], G=G, R=R, cases=complete_thm,
+        NominalFunctionResult {fs=[f], G=G, R=R, cases=complete_thm,
           psimps=psimps, simple_pinducts=[simple_pinduct],
-          termination=total_intro, domintros=dom_intros}
+          termination=total_intro, domintros=dom_intros, eqvts=[f_eqvt]}
       end
   in
     ((f, goalstate, mk_partial_rules), lthy)