nominal_primrec now prints initial proof state.

--- a/src/HOL/Nominal/nominal_primrec.ML	Mon Dec 11 16:06:59 2006 +0100
+++ b/src/HOL/Nominal/nominal_primrec.ML	Mon Dec 11 16:53:00 2006 +0100
@@ -431,7 +431,7 @@
 val primrecP =
   OuterSyntax.command "nominal_primrec" "define primitive recursive functions on nominal datatypes" K.thy_goal
     (primrec_decl >> (fn ((unchecked, (alt_name, (invs, fctxt))), eqns) =>
-      Toplevel.theory_to_proof
+      Toplevel.print o Toplevel.theory_to_proof
         ((if unchecked then add_primrec_unchecked else add_primrec) alt_name invs fctxt
           (map P.triple_swap eqns))));