# HG changeset patch
# User blanchet
# Date 1348244717 -7200
# Node ID 191d9384966ac8aaa8037ca9ed0037dc19de2c42
# Parent  45e3e564e306cc595141fbd398985440f75b2b44
fixed a few names that escaped the renaming

diff -r 45e3e564e306 -r 191d9384966a src/HOL/BNF/Tools/bnf_def.ML
--- a/src/HOL/BNF/Tools/bnf_def.ML	Fri Sep 21 18:25:17 2012 +0200
+++ b/src/HOL/BNF/Tools/bnf_def.ML	Fri Sep 21 18:25:17 2012 +0200
@@ -1026,10 +1026,10 @@
         val srel_cong = mk_lazy mk_srel_cong;
 
         fun mk_srel_Id () =
-          let val relAsAs = mk_bnf_srel self_setRTs CA' CA' in
+          let val srelAsAs = mk_bnf_srel self_setRTs CA' CA' in
             Skip_Proof.prove lthy [] []
               (HOLogic.mk_Trueprop
-                (HOLogic.mk_eq (Term.list_comb (relAsAs, map Id_const As'), Id_const CA')))
+                (HOLogic.mk_eq (Term.list_comb (srelAsAs, map Id_const As'), Id_const CA')))
               (mk_srel_Id_tac live (Lazy.force srel_Gr) (#map_id axioms))
             |> Thm.close_derivation
           end;
@@ -1038,8 +1038,8 @@
 
         fun mk_srel_converse () =
           let
-            val relBsAs = mk_bnf_srel setRT's CB' CA';
-            val lhs = Term.list_comb (relBsAs, map mk_converse Rs);
+            val srelBsAs = mk_bnf_srel setRT's CB' CA';
+            val lhs = Term.list_comb (srelBsAs, map mk_converse Rs);
             val rhs = mk_converse (Term.list_comb (srel, Rs));
             val le_goal = fold_rev Logic.all Rs (HOLogic.mk_Trueprop (mk_subset lhs rhs));
             val le_thm = Skip_Proof.prove lthy [] [] le_goal
@@ -1056,10 +1056,10 @@
 
         fun mk_srel_O () =
           let
-            val relAsCs = mk_bnf_srel setRTsAsCs CA' CC';
-            val relBsCs = mk_bnf_srel setRTsBsCs CB' CC';
-            val lhs = Term.list_comb (relAsCs, map2 (curry mk_rel_comp) Rs Ss);
-            val rhs = mk_rel_comp (Term.list_comb (srel, Rs), Term.list_comb (relBsCs, Ss));
+            val srelAsCs = mk_bnf_srel setRTsAsCs CA' CC';
+            val srelBsCs = mk_bnf_srel setRTsBsCs CB' CC';
+            val lhs = Term.list_comb (srelAsCs, map2 (curry mk_rel_comp) Rs Ss);
+            val rhs = mk_rel_comp (Term.list_comb (srel, Rs), Term.list_comb (srelBsCs, Ss));
             val goal = fold_rev Logic.all (Rs @ Ss) (mk_Trueprop_eq (lhs, rhs));
           in
             Skip_Proof.prove lthy [] [] goal
diff -r 45e3e564e306 -r 191d9384966a src/HOL/BNF/Tools/bnf_gfp.ML
--- a/src/HOL/BNF/Tools/bnf_gfp.ML	Fri Sep 21 18:25:17 2012 +0200
+++ b/src/HOL/BNF/Tools/bnf_gfp.ML	Fri Sep 21 18:25:17 2012 +0200
@@ -2885,10 +2885,10 @@
         val rels = map2 (fn Ds => mk_rel_of_bnf Ds (passiveAs @ Ts) (passiveBs @ Ts')) Dss bnfs;
         val Jrels = map (mk_rel_of_bnf deads passiveAs passiveBs) Jbnfs;
 
-        val JrelRs = map (fn Jsrel => Term.list_comb (Jsrel, JRs)) Jsrels;
-        val relRs = map (fn srel => Term.list_comb (srel, JRs @ JrelRs)) srels;
-        val Jpredphis = map (fn Jsrel => Term.list_comb (Jsrel, Jphis)) Jrels;
-        val predphis = map (fn srel => Term.list_comb (srel, Jphis @ Jpredphis)) rels;
+        val JsrelRs = map (fn Jsrel => Term.list_comb (Jsrel, JRs)) Jsrels;
+        val srelRs = map (fn srel => Term.list_comb (srel, JRs @ JsrelRs)) srels;
+        val Jrelphis = map (fn Jsrel => Term.list_comb (Jsrel, Jphis)) Jrels;
+        val relphis = map (fn srel => Term.list_comb (srel, Jphis @ Jrelphis)) rels;
 
         val in_srels = map in_srel_of_bnf bnfs;
         val in_Jsrels = map in_srel_of_bnf Jbnfs;
@@ -2901,10 +2901,10 @@
 
         val Jsrel_simp_thms =
           let
-            fun mk_goal Jz Jz' dtor dtor' JrelR relR = fold_rev Logic.all (Jz :: Jz' :: JRs)
-              (mk_Trueprop_eq (HOLogic.mk_mem (HOLogic.mk_prod (Jz, Jz'), JrelR),
-                  HOLogic.mk_mem (HOLogic.mk_prod (dtor $ Jz, dtor' $ Jz'), relR)));
-            val goals = map6 mk_goal Jzs Jz's dtors dtor's JrelRs relRs;
+            fun mk_goal Jz Jz' dtor dtor' JsrelR srelR = fold_rev Logic.all (Jz :: Jz' :: JRs)
+              (mk_Trueprop_eq (HOLogic.mk_mem (HOLogic.mk_prod (Jz, Jz'), JsrelR),
+                  HOLogic.mk_mem (HOLogic.mk_prod (dtor $ Jz, dtor' $ Jz'), srelR)));
+            val goals = map6 mk_goal Jzs Jz's dtors dtor's JsrelRs srelRs;
           in
             map12 (fn i => fn goal => fn in_srel => fn map_comp => fn map_cong =>
               fn map_simp => fn set_simps => fn dtor_inject => fn dtor_ctor =>
@@ -2921,7 +2921,7 @@
           let
             fun mk_goal Jz Jz' dtor dtor' Jpredphi predphi = fold_rev Logic.all (Jz :: Jz' :: Jphis)
               (mk_Trueprop_eq (Jpredphi $ Jz $ Jz', predphi $ (dtor $ Jz) $ (dtor' $ Jz')));
-            val goals = map6 mk_goal Jzs Jz's dtors dtor's Jpredphis predphis;
+            val goals = map6 mk_goal Jzs Jz's dtors dtor's Jrelphis relphis;
           in
             map3 (fn goal => fn srel_def => fn Jsrel_simp =>
               Skip_Proof.prove lthy [] [] goal
diff -r 45e3e564e306 -r 191d9384966a src/HOL/BNF/Tools/bnf_lfp.ML
--- a/src/HOL/BNF/Tools/bnf_lfp.ML	Fri Sep 21 18:25:17 2012 +0200
+++ b/src/HOL/BNF/Tools/bnf_lfp.ML	Fri Sep 21 18:25:17 2012 +0200
@@ -1725,10 +1725,10 @@
         val rels = map2 (fn Ds => mk_rel_of_bnf Ds (passiveAs @ Ts) (passiveBs @ Ts')) Dss bnfs;
         val Irels = map (mk_rel_of_bnf deads passiveAs passiveBs) Ibnfs;
 
-        val IrelRs = map (fn Isrel => Term.list_comb (Isrel, IRs)) Isrels;
-        val relRs = map (fn srel => Term.list_comb (srel, IRs @ IrelRs)) srels;
-        val Ipredphis = map (fn Isrel => Term.list_comb (Isrel, Iphis)) Irels;
-        val predphis = map (fn srel => Term.list_comb (srel, Iphis @ Ipredphis)) rels;
+        val IsrelRs = map (fn Isrel => Term.list_comb (Isrel, IRs)) Isrels;
+        val srelRs = map (fn srel => Term.list_comb (srel, IRs @ IsrelRs)) srels;
+        val Irelphis = map (fn Isrel => Term.list_comb (Isrel, Iphis)) Irels;
+        val relphis = map (fn srel => Term.list_comb (srel, Iphis @ Irelphis)) rels;
 
         val in_srels = map in_srel_of_bnf bnfs;
         val in_Isrels = map in_srel_of_bnf Ibnfs;
@@ -1744,10 +1744,10 @@
 
         val Isrel_simp_thms =
           let
-            fun mk_goal xF yF ctor ctor' IrelR relR = fold_rev Logic.all (xF :: yF :: IRs)
-              (mk_Trueprop_eq (HOLogic.mk_mem (HOLogic.mk_prod (ctor $ xF, ctor' $ yF), IrelR),
-                  HOLogic.mk_mem (HOLogic.mk_prod (xF, yF), relR)));
-            val goals = map6 mk_goal xFs yFs ctors ctor's IrelRs relRs;
+            fun mk_goal xF yF ctor ctor' IsrelR srelR = fold_rev Logic.all (xF :: yF :: IRs)
+              (mk_Trueprop_eq (HOLogic.mk_mem (HOLogic.mk_prod (ctor $ xF, ctor' $ yF), IsrelR),
+                  HOLogic.mk_mem (HOLogic.mk_prod (xF, yF), srelR)));
+            val goals = map6 mk_goal xFs yFs ctors ctor's IsrelRs srelRs;
           in
             map12 (fn i => fn goal => fn in_srel => fn map_comp => fn map_cong =>
               fn map_simp => fn set_simps => fn ctor_inject => fn ctor_dtor =>
@@ -1764,7 +1764,7 @@
           let
             fun mk_goal xF yF ctor ctor' Ipredphi predphi = fold_rev Logic.all (xF :: yF :: Iphis)
               (mk_Trueprop_eq (Ipredphi $ (ctor $ xF) $ (ctor' $ yF), predphi $ xF $ yF));
-            val goals = map6 mk_goal xFs yFs ctors ctor's Ipredphis predphis;
+            val goals = map6 mk_goal xFs yFs ctors ctor's Irelphis relphis;
           in
             map3 (fn goal => fn srel_def => fn Isrel_simp =>
               Skip_Proof.prove lthy [] [] goal
@@ -1784,10 +1784,10 @@
 
         val Ibnf_notes =
           [(map_simpsN, map single folded_map_simp_thms),
+          (rel_simpN, map single Irel_simp_thms),
           (set_inclN, set_incl_thmss),
           (set_set_inclN, map flat set_set_incl_thmsss),
-          (srel_simpN, map single Isrel_simp_thms),
-          (rel_simpN, map single Irel_simp_thms)] @
+          (srel_simpN, map single Isrel_simp_thms)] @
           map2 (fn i => fn thms => (mk_set_simpsN i, map single thms)) ls' folded_set_simp_thmss
           |> maps (fn (thmN, thmss) =>
             map2 (fn b => fn thms =>