# HG changeset patch
# User blanchet
# Date 1396342289 -7200
# Node ID b53d78fd25a38822994144e1b4a32649d400f19d
# Parent  2653b2fdad066e13b6ed18680138a3501de5198c
compile

diff -r 2653b2fdad06 -r b53d78fd25a3 src/HOL/Library/bnf_decl.ML
--- a/src/HOL/Library/bnf_decl.ML	Tue Apr 01 10:51:29 2014 +0200
+++ b/src/HOL/Library/bnf_decl.ML	Tue Apr 01 10:51:29 2014 +0200
@@ -88,8 +88,10 @@
       |> map (map (Thm.close_derivation o Thm.forall_elim_vars 0));
     val phi = Proof_Context.export_morphism lthy_old lthy;
     val thms = unflat all_goalss (Morphism.fact phi raw_thms);
+
+    val (bnf, lthy') = after_qed mk_wit_thms thms lthy
   in
-    BNF_Def.register_bnf key (after_qed mk_wit_thms thms lthy)
+    (bnf, BNF_Def.register_bnf key bnf lthy')
   end;
 
 val bnf_decl = prepare_decl (K I) (K I);