register pre-fixpoint BNFs in database to enable lookup later (e.g. in 'corec')

--- 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;