# HG changeset patch
# User blanchet
# Date 1348101768 -7200
# Node ID cca4390e8071bc32d53ef9342a8e2584890b363d
# Parent  ff0e540d875867de5f36df782c0611807a02102e
moved predicator definition before after_qed

diff -r ff0e540d8758 -r cca4390e8071 src/HOL/Codatatype/Tools/bnf_def.ML
--- a/src/HOL/Codatatype/Tools/bnf_def.ML	Thu Sep 20 02:42:48 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_def.ML	Thu Sep 20 02:42:48 2012 +0200
@@ -577,7 +577,6 @@
       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 =
@@ -657,6 +656,7 @@
     (*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'
@@ -731,6 +731,29 @@
       ||>> 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');
@@ -922,33 +945,6 @@
         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
@@ -1166,7 +1162,7 @@
                 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) =