src/HOL/Codatatype/Tools/bnf_def.ML

         val bs = if nwits = 1 then [fn () => Binding.suffix_name ("_" ^ witN) b]
           else map (fn i => fn () => Binding.suffix_name ("_" ^ mk_witN i) b) (1 upto nwits);
       in map2 pair bs wit_rhss end;
     val rel_bind_def = (fn () => Binding.suffix_name ("_" ^ relN) b, rel_rhs);
 
-    (* TODO: ### Kill "needed_for_extra_facts" *)
     fun maybe_define needed_for_extra_facts (b, rhs) lthy =
       let
         val inline =
           (not needed_for_extra_facts orelse fact_policy = Derive_Some_Facts) andalso
           (case const_policy of

     val dead = length deads;
 
     (*TODO: further checks of type of bnf_map*)
     (*TODO: check types of bnf_sets*)
     (*TODO: check type of bnf_bd*)
+    (*TODO: check type of bnf_rel*)
 
     val ((((((((((As', Bs'), Cs), Ds), B1Ts), B2Ts), domTs), ranTs), ranTs'), ranTs''),
       (Ts, T)) = lthy'
       |> mk_TFrees live
       ||>> mk_TFrees live

       ||>> mk_Frees "R" setRTs
       ||>> mk_Frees "R" setRTs
       ||>> mk_Frees "S" setRTsBsCs
       ||>> mk_Frees' "Q" QTs;
 
+    val pred_rhs = fold absfree (y' :: x' :: rev Qs') (HOLogic.mk_mem (HOLogic.mk_prod (x, y),
+      Term.list_comb (relAsBs, map3 (fn Q => fn T => fn U =>
+        HOLogic.Collect_const (HOLogic.mk_prodT (T, U)) $ HOLogic.mk_split Q)
+        Qs As' Bs')));
+    val pred_bind_def = (fn () => Binding.suffix_name ("_" ^ predN) b, pred_rhs);
+
+    val ((bnf_pred_term, raw_pred_def), (lthy''', lthy'')) =
+      lthy
+      |> maybe_define true pred_bind_def
+      ||> `(maybe_restore lthy');
+
+    val phi = Proof_Context.export_morphism lthy'' lthy''';
+    val bnf_pred = Morphism.term phi bnf_pred_term;
+
+    fun mk_bnf_pred QTs CA' CB' = normalize_pred lthy''' QTs CA' CB' bnf_pred;
+
+    val pred = mk_bnf_pred QTs CA' CB';
+    val bnf_pred_def =
+      if fact_policy <> Derive_Some_Facts then
+        mk_unabs_def (live + 2) (Morphism.thm phi raw_pred_def RS meta_eq_to_obj_eq)
+      else
+        no_fact;
+
     val goal_map_id =
       let
         val bnf_map_app_id = Term.list_comb (bnf_map_AsAs, map HOLogic.id_const As');
       in
         HOLogic.mk_Trueprop

         val map_id' = mk_lazy (fn () => mk_id' (#map_id axioms));
         val map_comp' = mk_lazy (fn () => mk_comp' (#map_comp axioms));
 
         val set_natural' =
           map (fn thm => mk_lazy (fn () => mk_set_natural' thm)) (#set_natural axioms);
-
-        (* predicator *)
-
-        val pred_rhs = fold absfree (y' :: x' :: rev Qs') (HOLogic.mk_mem (HOLogic.mk_prod (x, y),
-          Term.list_comb (relAsBs, map3 (fn Q => fn T => fn U =>
-            HOLogic.Collect_const (HOLogic.mk_prodT (T, U)) $ HOLogic.mk_split Q)
-            Qs As' Bs')));
-        val pred_bind_def = (fn () => Binding.suffix_name ("_" ^ predN) b, pred_rhs);
-
-        val ((bnf_pred_term, raw_pred_def), (lthy, lthy_old)) =
-          lthy
-          |> maybe_define true pred_bind_def
-          ||> `(maybe_restore lthy);
-
-        (*transforms defined frees into consts*)
-        val phi = Proof_Context.export_morphism lthy_old lthy;
-        val bnf_pred = Morphism.term phi bnf_pred_term;
-
-        fun mk_bnf_pred QTs CA' CB' = normalize_pred lthy QTs CA' CB' bnf_pred;
-
-        val pred = mk_bnf_pred QTs CA' CB';
-        val bnf_pred_def0 = Morphism.thm phi raw_pred_def;
-        val bnf_pred_def =
-          if fact_policy <> Derive_Some_Facts then
-            mk_unabs_def (live + 2) (bnf_pred_def0 RS meta_eq_to_obj_eq)
-          else
-            no_fact;
 
         fun mk_map_wppull () =
           let
             val prems = if live = 0 then [] else
               [HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj

                 end
               else
                 I))
       end;
   in
-    (key, goals, wit_goalss, after_qed, lthy', one_step_defs)
+    (key, goals, wit_goalss, after_qed, lthy''', one_step_defs)
   end;
 
 fun register_bnf key (bnf, lthy) =
   (bnf, Local_Theory.declaration {syntax = false, pervasive = true}
     (fn phi => Data.map (Symtab.update_new (key, morph_bnf phi bnf))) lthy);