--- a/Nominal/nominal_function.ML	Mon Jul 18 10:50:21 2011 +0100
+++ b/Nominal/nominal_function.ML	Mon Jul 18 17:40:13 2011 +0100
@@ -9,15 +9,15 @@
 
 signature NOMINAL_FUNCTION =
 sig
-  include FUNCTION_DATA
+  include NOMINAL_FUNCTION_DATA
 
   val add_nominal_function: (binding * typ option * mixfix) list ->
     (Attrib.binding * term) list ->  Nominal_Function_Common.nominal_function_config ->
-    (Proof.context -> tactic) -> local_theory -> info * local_theory
+    (Proof.context -> tactic) -> local_theory -> nominal_info * local_theory
 
   val add_nominal_function_cmd: (binding * string option * mixfix) list ->
     (Attrib.binding * string) list ->  Nominal_Function_Common.nominal_function_config ->
-    (Proof.context -> tactic) -> local_theory -> info * local_theory
+    (Proof.context -> tactic) -> local_theory -> nominal_info * local_theory
 
   val nominal_function: (binding * typ option * mixfix) list ->
     (Attrib.binding * term) list ->  Nominal_Function_Common.nominal_function_config ->
@@ -30,7 +30,7 @@
   val setup : theory -> theory
   val get_congs : Proof.context -> thm list
 
-  val get_info : Proof.context -> term -> info
+  val get_info : Proof.context -> term -> nominal_info
 end
 
 
@@ -152,9 +152,12 @@
 
     fun afterqed [[proof]] lthy =
       let
-        val FunctionResult {fs, R, psimps, simple_pinducts,
-          termination, domintros, cases, ...} =
+        val NominalFunctionResult {fs, R, psimps, simple_pinducts,
+          termination, domintros, cases, eqvts, ...} =
           cont (Thm.close_derivation proof)
+  
+        val _ = tracing ("final psimps:\n" ^ cat_lines (map @{make_string} psimps))
+        val _ = tracing ("final eqvts:\n" ^ cat_lines (map @{make_string} eqvts))
 
         val fnames = map (fst o fst) fixes
         fun qualify n = Binding.name n
@@ -179,7 +182,9 @@
 
         val info = { add_simps=addsmps, case_names=cnames, psimps=psimps',
           pinducts=snd pinducts', simps=NONE, inducts=NONE, termination=termination',
-          fs=fs, R=R, defname=defname, is_partial=true }
+          fs=fs, R=R, defname=defname, is_partial=true, eqvts=eqvts}
+
+        val _ = tracing ("final final psimps:\n" ^ cat_lines (map @{make_string} psimps'))
 
         val _ =
           if not is_external then ()