# HG changeset patch
# User blanchet
# Date 1427408584 -3600
# Node ID 0e9a0a5f4424649eaa7d068b6efc4ffaf47a3954
# Parent  dbec7f33093d49a0e23b5f6e54825be1d5c76a0a
register pre-fixpoint BNFs in database to enable lookup later (e.g. in 'corec')

diff -r dbec7f33093d -r 0e9a0a5f4424 src/HOL/Tools/BNF/bnf_comp.ML
--- a/src/HOL/Tools/BNF/bnf_comp.ML	Thu Mar 26 17:10:24 2015 +0100
+++ b/src/HOL/Tools/BNF/bnf_comp.ML	Thu Mar 26 23:23:04 2015 +0100
@@ -906,7 +906,9 @@
     val notes = (map_b, map_def) :: (rel_b, rel_def) :: (set_bs ~~ set_defs)
       |> map (fn (b, def) => ((b, []), [([def], [])]))
 
-    val (noted, lthy'') = lthy' |> Local_Theory.notes notes
+    val (noted, lthy'') = lthy'
+      |> Local_Theory.notes notes
+      ||> (if repTA = TA then I else register_bnf_raw (fst (dest_Type TA)) bnf'')
   in
     ((morph_bnf (substitute_noted_thm noted) bnf'', (all_deads, absT_info)), lthy'')
   end;