# HG changeset patch
# User berghofe
# Date 1165852380 -3600
# Node ID 78ed5e22766ace426e3805b8609c8fd3ff3221d2
# Parent  3eb48154388e422a4f8cb14209df3f061ce65215
nominal_primrec now prints initial proof state.

diff -r 3eb48154388e -r 78ed5e22766a src/HOL/Nominal/nominal_primrec.ML
--- 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))));