src/HOL/Library/bnf_axiomatization.ML

--- a/src/HOL/Library/bnf_axiomatization.ML	Fri Sep 05 00:41:01 2014 +0200
+++ b/src/HOL/Library/bnf_axiomatization.ML	Fri Sep 05 00:41:01 2014 +0200
@@ -91,7 +91,7 @@
 
     val (bnf, lthy') = after_qed mk_wit_thms thms lthy
   in
-    (bnf, BNF_Def.register_bnf key bnf lthy')
+    (bnf, BNF_Def.register_bnf (K true) key bnf lthy')
   end;
 
 val bnf_axiomatization = prepare_decl (K I) (K I);