--- a/Nominal/nominal_function_core.ML	Tue Aug 07 18:53:50 2012 +0100
+++ b/Nominal/nominal_function_core.ML	Tue Aug 07 18:54:52 2012 +0100
@@ -18,10 +18,15 @@
     -> ((bstring * typ) list * term list * term * term) list (* specification *)
     -> local_theory
     -> (term   (* f *)
+        * term (* G(raph) *)
+        * thm list (* GIntros *)
+        * thm (* Ginduct *) 
         * thm  (* goalstate *)
         * (thm -> Nominal_Function_Common.nominal_function_result) (* continuation *)
        ) * local_theory
 
+  val inductive_def : (binding * typ) * mixfix -> term list -> local_theory 
+    -> (term * thm list * thm * thm) * local_theory
 end
 
 structure Nominal_Function_Core : NOMINAL_FUNCTION_CORE =
@@ -586,7 +591,7 @@
 
 (* wrapper -- restores quantifiers in rule specifications *)
 fun inductive_def (binding as ((R, T), _)) intrs lthy =
-  let
+  let 
     val ({intrs = intrs_gen, elims = [elim_gen], preds = [ Rdef ], induct, raw_induct, ...}, lthy) =
       lthy
       |> Local_Theory.conceal
@@ -1083,7 +1088,7 @@
           termination=total_intro, domintros=dom_intros, eqvts=[f_eqvt]}
       end
   in
-    ((f, goalstate, mk_partial_rules), lthy)
+    ((f, G, GIntro_thms, G_induct, goalstate, mk_partial_rules), lthy)
   end