# HG changeset patch
# User blanchet
# Date 1348235609 -7200
# Node ID aeb0cc8889f262e85139cad3f439cdd0695b33c9
# Parent  a944eefb67e671c35629b93ec29e05cf97ee7343
renamed "rel" to "srel"

diff -r a944eefb67e6 -r aeb0cc8889f2 src/HOL/Codatatype/Tools/bnf_comp.ML
--- a/src/HOL/Codatatype/Tools/bnf_comp.ML	Fri Sep 21 15:53:29 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_comp.ML	Fri Sep 21 15:53:29 2012 +0200
@@ -13,7 +13,7 @@
   val map_unfolds_of: unfold_set -> thm list
   val set_unfoldss_of: unfold_set -> thm list list
   val pred_unfolds_of: unfold_set -> thm list
-  val rel_unfolds_of: unfold_set -> thm list
+  val srel_unfolds_of: unfold_set -> thm list
 
   val bnf_of_typ: BNF_Def.const_policy -> (binding -> binding) ->
     ((string * sort) list list -> (string * sort) list) -> typ -> unfold_set * Proof.context ->
@@ -38,29 +38,29 @@
   map_unfolds: thm list,
   set_unfoldss: thm list list,
   pred_unfolds: thm list,
-  rel_unfolds: thm list
+  srel_unfolds: thm list
 };
 
-val empty_unfolds = {map_unfolds = [], set_unfoldss = [], pred_unfolds = [], rel_unfolds = []};
+val empty_unfolds = {map_unfolds = [], set_unfoldss = [], pred_unfolds = [], srel_unfolds = []};
 
 fun add_to_thms thms new = thms |> not (Thm.is_reflexive new) ? insert Thm.eq_thm new;
 fun adds_to_thms thms news = insert (eq_set Thm.eq_thm) (no_reflexive news) thms;
 
-fun add_to_unfolds map sets pred rel
-  {map_unfolds, set_unfoldss, pred_unfolds, rel_unfolds} =
+fun add_to_unfolds map sets pred srel
+  {map_unfolds, set_unfoldss, pred_unfolds, srel_unfolds} =
   {map_unfolds = add_to_thms map_unfolds map,
     set_unfoldss = adds_to_thms set_unfoldss sets,
     pred_unfolds = add_to_thms pred_unfolds pred,
-    rel_unfolds = add_to_thms rel_unfolds rel};
+    srel_unfolds = add_to_thms srel_unfolds srel};
 
 fun add_bnf_to_unfolds bnf =
   add_to_unfolds (map_def_of_bnf bnf) (set_defs_of_bnf bnf) (pred_def_of_bnf bnf)
-    (rel_def_of_bnf bnf);
+    (srel_def_of_bnf bnf);
 
 val map_unfolds_of = #map_unfolds;
 val set_unfoldss_of = #set_unfoldss;
 val pred_unfolds_of = #pred_unfolds;
-val rel_unfolds_of = #rel_unfolds;
+val srel_unfolds_of = #srel_unfolds;
 
 val bdTN = "bdT";
 
@@ -230,25 +230,25 @@
     fun map_wpull_tac _ =
       mk_map_wpull_tac in_alt_thm (map map_wpull_of_bnf inners) (map_wpull_of_bnf outer);
 
-    fun rel_O_Gr_tac _ =
+    fun srel_O_Gr_tac _ =
       let
         val basic_thms = @{thms mem_Collect_eq fst_conv snd_conv}; (*TODO: tune*)
-        val outer_rel_Gr = rel_Gr_of_bnf outer RS sym;
-        val outer_rel_cong = rel_cong_of_bnf outer;
+        val outer_srel_Gr = srel_Gr_of_bnf outer RS sym;
+        val outer_srel_cong = srel_cong_of_bnf outer;
         val thm =
           (trans OF [in_alt_thm RS @{thm subst_rel_def},
              trans OF [@{thm arg_cong2[of _ _ _ _ relcomp]} OF
-               [trans OF [outer_rel_Gr RS @{thm arg_cong[of _ _ converse]},
-                 rel_converse_of_bnf outer RS sym], outer_rel_Gr],
-               trans OF [rel_O_of_bnf outer RS sym, outer_rel_cong OF
-                 (map (fn bnf => rel_O_Gr_of_bnf bnf RS sym) inners)]]] RS sym)
-          |> unfold_thms lthy (basic_thms @ rel_def_of_bnf outer :: map rel_def_of_bnf inners);
+               [trans OF [outer_srel_Gr RS @{thm arg_cong[of _ _ converse]},
+                 srel_converse_of_bnf outer RS sym], outer_srel_Gr],
+               trans OF [srel_O_of_bnf outer RS sym, outer_srel_cong OF
+                 (map (fn bnf => srel_O_Gr_of_bnf bnf RS sym) inners)]]] RS sym)
+          |> unfold_thms lthy (basic_thms @ srel_def_of_bnf outer :: map srel_def_of_bnf inners);
       in
         unfold_thms_tac lthy basic_thms THEN rtac thm 1
       end;
 
     val tacs = zip_axioms map_id_tac map_comp_tac map_cong_tac set_natural_tacs bd_card_order_tac
-      bd_cinfinite_tac set_bd_tacs in_bd_tac map_wpull_tac rel_O_Gr_tac;
+      bd_cinfinite_tac set_bd_tacs in_bd_tac map_wpull_tac srel_O_Gr_tac;
 
     val outer_wits = mk_wits_of_bnf (replicate onwits oDs) (replicate onwits CAs) outer;
 
@@ -341,24 +341,24 @@
         (bd_Cinfinite_of_bnf bnf) (bd_Cnotzero_of_bnf bnf);
     fun map_wpull_tac _ = mk_map_wpull_tac in_alt_thm [] (map_wpull_of_bnf bnf);
 
-    fun rel_O_Gr_tac _ =
+    fun srel_O_Gr_tac _ =
       let
-        val rel_Gr = rel_Gr_of_bnf bnf RS sym
+        val srel_Gr = srel_Gr_of_bnf bnf RS sym
         val thm =
           (trans OF [in_alt_thm RS @{thm subst_rel_def},
             trans OF [@{thm arg_cong2[of _ _ _ _ relcomp]} OF
-              [trans OF [rel_Gr RS @{thm arg_cong[of _ _ converse]},
-                rel_converse_of_bnf bnf RS sym], rel_Gr],
-              trans OF [rel_O_of_bnf bnf RS sym, rel_cong_of_bnf bnf OF
+              [trans OF [srel_Gr RS @{thm arg_cong[of _ _ converse]},
+                srel_converse_of_bnf bnf RS sym], srel_Gr],
+              trans OF [srel_O_of_bnf bnf RS sym, srel_cong_of_bnf bnf OF
                 (replicate n @{thm trans[OF Gr_UNIV_id[OF refl] Id_alt[symmetric]]} @
                  replicate (live - n) @{thm Gr_fst_snd})]]] RS sym)
-          |> unfold_thms lthy (rel_def_of_bnf bnf :: @{thms Id_def' mem_Collect_eq split_conv});
+          |> unfold_thms lthy (srel_def_of_bnf bnf :: @{thms Id_def' mem_Collect_eq split_conv});
       in
         rtac thm 1
       end;
 
     val tacs = zip_axioms map_id_tac map_comp_tac map_cong_tac set_natural_tacs bd_card_order_tac
-      bd_cinfinite_tac set_bd_tacs in_bd_tac map_wpull_tac rel_O_Gr_tac;
+      bd_cinfinite_tac set_bd_tacs in_bd_tac map_wpull_tac srel_O_Gr_tac;
 
     val bnf_wits = mk_wits_of_bnf (replicate nwits Ds) (replicate nwits As) bnf;
 
@@ -441,11 +441,11 @@
     fun in_bd_tac _ = mk_lift_in_bd_tac n in_alt_thm (in_bd_of_bnf bnf) (bd_Card_order_of_bnf bnf);
     fun map_wpull_tac _ = mk_map_wpull_tac in_alt_thm [] (map_wpull_of_bnf bnf);
 
-    fun rel_O_Gr_tac _ =
-      mk_simple_rel_O_Gr_tac lthy (rel_def_of_bnf bnf) (rel_O_Gr_of_bnf bnf) in_alt_thm;
+    fun srel_O_Gr_tac _ =
+      mk_simple_srel_O_Gr_tac lthy (srel_def_of_bnf bnf) (srel_O_Gr_of_bnf bnf) in_alt_thm;
 
     val tacs = zip_axioms map_id_tac map_comp_tac map_cong_tac set_natural_tacs bd_card_order_tac
-      bd_cinfinite_tac set_bd_tacs in_bd_tac map_wpull_tac rel_O_Gr_tac;
+      bd_cinfinite_tac set_bd_tacs in_bd_tac map_wpull_tac srel_O_Gr_tac;
 
     val wits = map snd (mk_wits_of_bnf (replicate nwits Ds) (replicate nwits As) bnf);
 
@@ -518,11 +518,11 @@
       mk_permute_in_bd_tac src dest in_alt_thm (in_bd_of_bnf bnf) (bd_Card_order_of_bnf bnf);
     fun map_wpull_tac _ = mk_map_wpull_tac in_alt_thm [] (map_wpull_of_bnf bnf);
 
-    fun rel_O_Gr_tac _ =
-      mk_simple_rel_O_Gr_tac lthy (rel_def_of_bnf bnf) (rel_O_Gr_of_bnf bnf) in_alt_thm;
+    fun srel_O_Gr_tac _ =
+      mk_simple_srel_O_Gr_tac lthy (srel_def_of_bnf bnf) (srel_O_Gr_of_bnf bnf) in_alt_thm;
 
     val tacs = zip_axioms map_id_tac map_comp_tac map_cong_tac set_natural_tacs bd_card_order_tac
-      bd_cinfinite_tac set_bd_tacs in_bd_tac map_wpull_tac rel_O_Gr_tac;
+      bd_cinfinite_tac set_bd_tacs in_bd_tac map_wpull_tac srel_O_Gr_tac;
 
     val wits = map snd (mk_wits_of_bnf (replicate nwits Ds) (replicate nwits As) bnf);
 
@@ -607,7 +607,7 @@
     val map_unfolds = map_unfolds_of unfold_set;
     val set_unfoldss = set_unfoldss_of unfold_set;
     val pred_unfolds = pred_unfolds_of unfold_set;
-    val rel_unfolds = rel_unfolds_of unfold_set;
+    val srel_unfolds = srel_unfolds_of unfold_set;
 
     val expand_maps = fold expand_term_const (map (single o Logic.dest_equals o Thm.prop_of)
       map_unfolds);
@@ -618,8 +618,8 @@
     val unfold_maps = fold (unfold_thms lthy o single) map_unfolds;
     val unfold_sets = fold (unfold_thms lthy) set_unfoldss;
     val unfold_preds = unfold_thms lthy pred_unfolds;
-    val unfold_rels = unfold_thms lthy rel_unfolds;
-    val unfold_all = unfold_sets o unfold_maps o unfold_preds o unfold_rels;
+    val unfold_srels = unfold_thms lthy srel_unfolds;
+    val unfold_all = unfold_sets o unfold_maps o unfold_preds o unfold_srels;
     val bnf_map = expand_maps (mk_map_of_bnf Ds As Bs bnf);
     val bnf_sets = map (expand_maps o expand_sets)
       (mk_sets_of_bnf (replicate live Ds) (replicate live As) bnf);
@@ -665,7 +665,7 @@
       (mk_tac (map_cong_of_bnf bnf)) (map mk_tac (set_natural_of_bnf bnf))
       (K (rtac bd_card_order 1)) (K (rtac bd_cinfinite 1)) (map mk_tac set_bds) (mk_tac in_bd)
       (mk_tac (map_wpull_of_bnf bnf))
-      (mk_tac (unfold_thms lthy [rel_def_of_bnf bnf] (rel_O_Gr_of_bnf bnf)));
+      (mk_tac (unfold_thms lthy [srel_def_of_bnf bnf] (srel_O_Gr_of_bnf bnf)));
 
     val bnf_wits = map snd (mk_wits_of_bnf (replicate nwits Ds) (replicate nwits As) bnf);
 
diff -r a944eefb67e6 -r aeb0cc8889f2 src/HOL/Codatatype/Tools/bnf_comp_tactics.ML
--- a/src/HOL/Codatatype/Tools/bnf_comp_tactics.ML	Fri Sep 21 15:53:29 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_comp_tactics.ML	Fri Sep 21 15:53:29 2012 +0200
@@ -35,7 +35,7 @@
   val mk_permute_in_bd_tac: ''a list -> ''a list -> thm -> thm -> thm -> tactic
 
   val mk_map_wpull_tac: thm -> thm list -> thm -> tactic
-  val mk_simple_rel_O_Gr_tac: Proof.context -> thm -> thm -> thm -> tactic
+  val mk_simple_srel_O_Gr_tac: Proof.context -> thm -> thm -> thm -> tactic
   val mk_simple_wit_tac: thm list -> tactic
 end;
 
@@ -407,9 +407,9 @@
   WRAP (fn thm => rtac thm 1 THEN REPEAT_DETERM (atac 1)) (K all_tac) inner_map_wpulls all_tac THEN
   TRY (REPEAT_DETERM (atac 1 ORELSE rtac @{thm wpull_id} 1));
 
-fun mk_simple_rel_O_Gr_tac ctxt rel_def rel_O_Gr in_alt_thm =
-  rtac (unfold_thms ctxt [rel_def] (trans OF [rel_O_Gr, in_alt_thm RS @{thm subst_rel_def} RS sym]))
-    1;
+fun mk_simple_srel_O_Gr_tac ctxt srel_def srel_O_Gr in_alt_thm =
+  rtac (unfold_thms ctxt [srel_def]
+    (trans OF [srel_O_Gr, in_alt_thm RS @{thm subst_rel_def} RS sym])) 1;
 
 fun mk_simple_wit_tac wit_thms = ALLGOALS (atac ORELSE' eresolve_tac (@{thm emptyE} :: wit_thms));
 
diff -r a944eefb67e6 -r aeb0cc8889f2 src/HOL/Codatatype/Tools/bnf_def.ML
--- a/src/HOL/Codatatype/Tools/bnf_def.ML	Fri Sep 21 15:53:29 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_def.ML	Fri Sep 21 15:53:29 2012 +0200
@@ -25,8 +25,8 @@
   val mapN: string
   val setN: string
   val predN: string
-  val relN: string
   val mk_setN: int -> string
+  val srelN: string
 
   val map_of_bnf: BNF -> term
 
@@ -34,8 +34,8 @@
   val mk_bd_of_bnf: typ list -> typ list -> BNF -> term
   val mk_map_of_bnf: typ list -> typ list -> typ list -> BNF -> term
   val mk_pred_of_bnf: typ list -> typ list -> typ list -> BNF -> term
-  val mk_rel_of_bnf: typ list -> typ list -> typ list -> BNF -> term
   val mk_sets_of_bnf: typ list list -> typ list list -> BNF -> term list
+  val mk_srel_of_bnf: typ list -> typ list -> typ list -> BNF -> term
   val mk_wits_of_bnf: typ list list -> typ list list -> BNF -> (int list * term) list
 
   val bd_Card_order_of_bnf: BNF -> thm
@@ -47,7 +47,7 @@
   val in_bd_of_bnf: BNF -> thm
   val in_cong_of_bnf: BNF -> thm
   val in_mono_of_bnf: BNF -> thm
-  val in_rel_of_bnf: BNF -> thm
+  val in_srel_of_bnf: BNF -> thm
   val map_comp'_of_bnf: BNF -> thm
   val map_comp_of_bnf: BNF -> thm
   val map_cong_of_bnf: BNF -> thm
@@ -57,19 +57,19 @@
   val map_wppull_of_bnf: BNF -> thm
   val map_wpull_of_bnf: BNF -> thm
   val pred_def_of_bnf: BNF -> thm
-  val rel_def_of_bnf: BNF -> thm
-  val rel_Gr_of_bnf: BNF -> thm
-  val rel_Id_of_bnf: BNF -> thm
-  val rel_O_of_bnf: BNF -> thm
-  val rel_O_Gr_of_bnf: BNF -> thm
-  val rel_cong_of_bnf: BNF -> thm
-  val rel_converse_of_bnf: BNF -> thm
-  val rel_mono_of_bnf: BNF -> thm
   val set_bd_of_bnf: BNF -> thm list
   val set_defs_of_bnf: BNF -> thm list
   val set_natural'_of_bnf: BNF -> thm list
   val set_natural_of_bnf: BNF -> thm list
   val sets_of_bnf: BNF -> term list
+  val srel_def_of_bnf: BNF -> thm
+  val srel_Gr_of_bnf: BNF -> thm
+  val srel_Id_of_bnf: BNF -> thm
+  val srel_O_of_bnf: BNF -> thm
+  val srel_O_Gr_of_bnf: BNF -> thm
+  val srel_cong_of_bnf: BNF -> thm
+  val srel_converse_of_bnf: BNF -> thm
+  val srel_mono_of_bnf: BNF -> thm
   val wit_thms_of_bnf: BNF -> thm list
   val wit_thmss_of_bnf: BNF -> thm list list
 
@@ -110,12 +110,12 @@
   set_bd: thm list,
   in_bd: thm,
   map_wpull: thm,
-  rel_O_Gr: thm
+  srel_O_Gr: thm
 };
 
-fun mk_axioms' (((((((((id, comp), cong), nat), c_o), cinf), set_bd), in_bd), wpull), rel) =
+fun mk_axioms' (((((((((id, comp), cong), nat), c_o), cinf), set_bd), in_bd), wpull), srel) =
   {map_id = id, map_comp = comp, map_cong = cong, set_natural = nat, bd_card_order = c_o,
-   bd_cinfinite = cinf, set_bd = set_bd, in_bd = in_bd, map_wpull = wpull, rel_O_Gr = rel};
+   bd_cinfinite = cinf, set_bd = set_bd, in_bd = in_bd, map_wpull = wpull, srel_O_Gr = srel};
 
 fun dest_cons [] = raise Empty
   | dest_cons (x :: xs) = (x, xs);
@@ -134,16 +134,16 @@
   ||> the_single
   |> mk_axioms';
 
-fun zip_axioms mid mcomp mcong snat bdco bdinf sbd inbd wpull rel =
-  [mid, mcomp, mcong] @ snat @ [bdco, bdinf] @ sbd @ [inbd, wpull, rel];
+fun zip_axioms mid mcomp mcong snat bdco bdinf sbd inbd wpull srel =
+  [mid, mcomp, mcong] @ snat @ [bdco, bdinf] @ sbd @ [inbd, wpull, srel];
 
 fun dest_axioms {map_id, map_comp, map_cong, set_natural, bd_card_order, bd_cinfinite, set_bd,
-  in_bd, map_wpull, rel_O_Gr} =
+  in_bd, map_wpull, srel_O_Gr} =
   zip_axioms map_id map_comp map_cong set_natural bd_card_order bd_cinfinite set_bd in_bd map_wpull
-    rel_O_Gr;
+    srel_O_Gr;
 
 fun map_axioms f {map_id, map_comp, map_cong, set_natural, bd_card_order, bd_cinfinite, set_bd,
-  in_bd, map_wpull, rel_O_Gr} =
+  in_bd, map_wpull, srel_O_Gr} =
   {map_id = f map_id,
     map_comp = f map_comp,
     map_cong = f map_cong,
@@ -153,7 +153,7 @@
     set_bd = map f set_bd,
     in_bd = f in_bd,
     map_wpull = f map_wpull,
-    rel_O_Gr = f rel_O_Gr};
+    srel_O_Gr = f srel_O_Gr};
 
 val morph_axioms = map_axioms o Morphism.thm;
 
@@ -161,13 +161,13 @@
   map_def: thm,
   set_defs: thm list,
   pred_def: thm,
-  rel_def: thm
+  srel_def: thm
 }
 
-fun mk_defs map sets pred rel = {map_def = map, set_defs = sets, pred_def = pred, rel_def = rel};
+fun mk_defs map sets pred srel = {map_def = map, set_defs = sets, pred_def = pred, srel_def = srel};
 
-fun map_defs f {map_def, set_defs, pred_def, rel_def} =
-  {map_def = f map_def, set_defs = map f set_defs, pred_def = f pred_def, rel_def = f rel_def};
+fun map_defs f {map_def, set_defs, pred_def, srel_def} =
+  {map_def = f map_def, set_defs = map f set_defs, pred_def = f pred_def, srel_def = f srel_def};
 
 val morph_defs = map_defs o Morphism.thm;
 
@@ -178,39 +178,39 @@
   collect_set_natural: thm lazy,
   in_cong: thm lazy,
   in_mono: thm lazy,
-  in_rel: thm lazy,
+  in_srel: thm lazy,
   map_comp': thm lazy,
   map_id': thm lazy,
   map_wppull: thm lazy,
-  rel_cong: thm lazy,
-  rel_mono: thm lazy,
-  rel_Id: thm lazy,
-  rel_Gr: thm lazy,
-  rel_converse: thm lazy,
-  rel_O: thm lazy,
-  set_natural': thm lazy list
+  set_natural': thm lazy list,
+  srel_cong: thm lazy,
+  srel_mono: thm lazy,
+  srel_Id: thm lazy,
+  srel_Gr: thm lazy,
+  srel_converse: thm lazy,
+  srel_O: thm lazy
 };
 
-fun mk_facts bd_Card_order bd_Cinfinite bd_Cnotzero
-    collect_set_natural in_cong in_mono in_rel map_comp' map_id' map_wppull
-    rel_cong rel_mono rel_Id rel_Gr rel_converse rel_O set_natural' = {
+fun mk_facts bd_Card_order bd_Cinfinite bd_Cnotzero collect_set_natural in_cong in_mono in_srel
+    map_comp' map_id' map_wppull set_natural' srel_cong srel_mono srel_Id srel_Gr srel_converse
+    srel_O = {
   bd_Card_order = bd_Card_order,
   bd_Cinfinite = bd_Cinfinite,
   bd_Cnotzero = bd_Cnotzero,
   collect_set_natural = collect_set_natural,
   in_cong = in_cong,
   in_mono = in_mono,
-  in_rel = in_rel,
+  in_srel = in_srel,
   map_comp' = map_comp',
   map_id' = map_id',
   map_wppull = map_wppull,
-  rel_cong = rel_cong,
-  rel_mono = rel_mono,
-  rel_Id = rel_Id,
-  rel_Gr = rel_Gr,
-  rel_converse = rel_converse,
-  rel_O = rel_O,
-  set_natural' = set_natural'};
+  set_natural' = set_natural',
+  srel_cong = srel_cong,
+  srel_mono = srel_mono,
+  srel_Id = srel_Id,
+  srel_Gr = srel_Gr,
+  srel_converse = srel_converse,
+  srel_O = srel_O};
 
 fun map_facts f {
   bd_Card_order,
@@ -219,34 +219,34 @@
   collect_set_natural,
   in_cong,
   in_mono,
-  in_rel,
+  in_srel,
   map_comp',
   map_id',
   map_wppull,
-  rel_cong,
-  rel_mono,
-  rel_Id,
-  rel_Gr,
-  rel_converse,
-  rel_O,
-  set_natural'} =
+  set_natural',
+  srel_cong,
+  srel_mono,
+  srel_Id,
+  srel_Gr,
+  srel_converse,
+  srel_O} =
   {bd_Card_order = f bd_Card_order,
     bd_Cinfinite = f bd_Cinfinite,
     bd_Cnotzero = f bd_Cnotzero,
     collect_set_natural = Lazy.map f collect_set_natural,
     in_cong = Lazy.map f in_cong,
     in_mono = Lazy.map f in_mono,
-    in_rel = Lazy.map f in_rel,
+    in_srel = Lazy.map f in_srel,
     map_comp' = Lazy.map f map_comp',
     map_id' = Lazy.map f map_id',
     map_wppull = Lazy.map f map_wppull,
-    rel_cong = Lazy.map f rel_cong,
-    rel_mono = Lazy.map f rel_mono,
-    rel_Id = Lazy.map f rel_Id,
-    rel_Gr = Lazy.map f rel_Gr,
-    rel_converse = Lazy.map f rel_converse,
-    rel_O = Lazy.map f rel_O,
-    set_natural' = map (Lazy.map f) set_natural'};
+    set_natural' = map (Lazy.map f) set_natural',
+    srel_cong = Lazy.map f srel_cong,
+    srel_mono = Lazy.map f srel_mono,
+    srel_Id = Lazy.map f srel_Id,
+    srel_Gr = Lazy.map f srel_Gr,
+    srel_converse = Lazy.map f srel_converse,
+    srel_O = Lazy.map f srel_O};
 
 val morph_facts = map_facts o Morphism.thm;
 
@@ -277,7 +277,7 @@
   nwits: int,
   wits: nonemptiness_witness list,
   pred: term,
-  rel: term
+  srel: term
 };
 
 (* getters *)
@@ -331,12 +331,12 @@
     Term.subst_atomic_types
       ((#deads bnf_rep ~~ Ds) @ (#lives bnf_rep ~~ Ts) @ (#lives' bnf_rep ~~ Us)) (#pred bnf_rep)
   end;
-val rel_of_bnf = #rel o rep_bnf;
-fun mk_rel_of_bnf Ds Ts Us bnf =
+val srel_of_bnf = #srel o rep_bnf;
+fun mk_srel_of_bnf Ds Ts Us bnf =
   let val bnf_rep = rep_bnf bnf;
   in
     Term.subst_atomic_types
-      ((#deads bnf_rep ~~ Ds) @ (#lives bnf_rep ~~ Ts) @ (#lives' bnf_rep ~~ Us)) (#rel bnf_rep)
+      ((#deads bnf_rep ~~ Ds) @ (#lives bnf_rep ~~ Ts) @ (#lives' bnf_rep ~~ Us)) (#srel bnf_rep)
   end;
 
 (*thms*)
@@ -349,7 +349,7 @@
 val in_bd_of_bnf = #in_bd o #axioms o rep_bnf;
 val in_cong_of_bnf = Lazy.force o #in_cong o #facts o rep_bnf;
 val in_mono_of_bnf = Lazy.force o #in_mono o #facts o rep_bnf;
-val in_rel_of_bnf = Lazy.force o #in_rel o #facts o rep_bnf;
+val in_srel_of_bnf = Lazy.force o #in_srel o #facts o rep_bnf;
 val map_def_of_bnf = #map_def o #defs o rep_bnf;
 val map_id_of_bnf = #map_id o #axioms o rep_bnf;
 val map_id'_of_bnf = Lazy.force o #map_id' o #facts o rep_bnf;
@@ -359,32 +359,32 @@
 val map_wppull_of_bnf = Lazy.force o #map_wppull o #facts o rep_bnf;
 val map_wpull_of_bnf = #map_wpull o #axioms o rep_bnf;
 val pred_def_of_bnf = #pred_def o #defs o rep_bnf;
-val rel_cong_of_bnf = Lazy.force o #rel_cong o #facts o rep_bnf;
-val rel_mono_of_bnf = Lazy.force o #rel_mono o #facts o rep_bnf;
-val rel_def_of_bnf = #rel_def o #defs o rep_bnf;
-val rel_Id_of_bnf = Lazy.force o #rel_Id o #facts o rep_bnf;
-val rel_Gr_of_bnf = Lazy.force o #rel_Gr o #facts o rep_bnf;
-val rel_converse_of_bnf = Lazy.force o #rel_converse o #facts o rep_bnf;
-val rel_O_of_bnf = Lazy.force o #rel_O o #facts o rep_bnf;
-val rel_O_Gr_of_bnf = #rel_O_Gr o #axioms o rep_bnf;
 val set_bd_of_bnf = #set_bd o #axioms o rep_bnf;
 val set_defs_of_bnf = #set_defs o #defs o rep_bnf;
 val set_natural_of_bnf = #set_natural o #axioms o rep_bnf;
 val set_natural'_of_bnf = map Lazy.force o #set_natural' o #facts o rep_bnf;
+val srel_cong_of_bnf = Lazy.force o #srel_cong o #facts o rep_bnf;
+val srel_mono_of_bnf = Lazy.force o #srel_mono o #facts o rep_bnf;
+val srel_def_of_bnf = #srel_def o #defs o rep_bnf;
+val srel_Id_of_bnf = Lazy.force o #srel_Id o #facts o rep_bnf;
+val srel_Gr_of_bnf = Lazy.force o #srel_Gr o #facts o rep_bnf;
+val srel_converse_of_bnf = Lazy.force o #srel_converse o #facts o rep_bnf;
+val srel_O_of_bnf = Lazy.force o #srel_O o #facts o rep_bnf;
+val srel_O_Gr_of_bnf = #srel_O_Gr o #axioms o rep_bnf;
 val wit_thms_of_bnf = maps #prop o wits_of_bnf;
 val wit_thmss_of_bnf = map #prop o wits_of_bnf;
 
-fun mk_bnf name T live lives lives' dead deads map sets bd axioms defs facts wits pred rel =
+fun mk_bnf name T live lives lives' dead deads map sets bd axioms defs facts wits pred srel =
   BNF {name = name, T = T,
        live = live, lives = lives, lives' = lives', dead = dead, deads = deads,
        map = map, sets = sets, bd = bd,
        axioms = axioms, defs = defs, facts = facts,
-       nwits = length wits, wits = wits, pred = pred, rel = rel};
+       nwits = length wits, wits = wits, pred = pred, srel = srel};
 
 fun morph_bnf phi (BNF {name = name, T = T, live = live, lives = lives, lives' = lives',
   dead = dead, deads = deads, map = map, sets = sets, bd = bd,
   axioms = axioms, defs = defs, facts = facts,
-  nwits = nwits, wits = wits, pred = pred, rel = rel}) =
+  nwits = nwits, wits = wits, pred = pred, srel = srel}) =
   BNF {name = Morphism.binding phi name, T = Morphism.typ phi T,
     live = live, lives = List.map (Morphism.typ phi) lives,
     lives' = List.map (Morphism.typ phi) lives',
@@ -396,7 +396,7 @@
     facts = morph_facts phi facts,
     nwits = nwits,
     wits = List.map (morph_witness phi) wits,
-    pred = Morphism.term phi pred, rel = Morphism.term phi rel};
+    pred = Morphism.term phi pred, srel = Morphism.term phi srel};
 
 fun eq_bnf (BNF {T = T1, live = live1, dead = dead1, ...},
   BNF {T = T2, live = live2, dead = dead2, ...}) =
@@ -432,13 +432,13 @@
   in Envir.subst_term (tyenv, Vartab.empty) pred end
   handle Type.TYPE_MATCH => error "Bad predicator";
 
-fun normalize_rel ctxt instTs instA instB rel =
+fun normalize_srel ctxt instTs instA instB srel =
   let
     val thy = Proof_Context.theory_of ctxt;
     val tyenv =
-      Sign.typ_match thy (fastype_of rel, Library.foldr (op -->) (instTs, mk_relT (instA, instB)))
+      Sign.typ_match thy (fastype_of srel, Library.foldr (op -->) (instTs, mk_relT (instA, instB)))
         Vartab.empty;
-  in Envir.subst_term (tyenv, Vartab.empty) rel end
+  in Envir.subst_term (tyenv, Vartab.empty) srel end
   handle Type.TYPE_MATCH => error "Bad relator";
 
 fun normalize_wit insts CA As wit =
@@ -473,7 +473,7 @@
 val witN = "wit";
 fun mk_witN i = witN ^ nonzero_string_of_int i;
 val predN = "pred";
-val relN = "rel";
+val srelN = "srel";
 
 val bd_card_orderN = "bd_card_order";
 val bd_cinfiniteN = "bd_cinfinite";
@@ -483,19 +483,19 @@
 val collect_set_naturalN = "collect_set_natural";
 val in_bdN = "in_bd";
 val in_monoN = "in_mono";
-val in_relN = "in_rel";
+val in_srelN = "in_srel";
 val map_idN = "map_id";
 val map_id'N = "map_id'";
 val map_compN = "map_comp";
 val map_comp'N = "map_comp'";
 val map_congN = "map_cong";
 val map_wpullN = "map_wpull";
-val rel_IdN = "rel_Id";
-val rel_GrN = "rel_Gr";
-val rel_converseN = "rel_converse";
-val rel_monoN = "rel_mono"
-val rel_ON = "rel_comp";
-val rel_O_GrN = "rel_comp_Gr";
+val srel_IdN = "srel_Id";
+val srel_GrN = "srel_Gr";
+val srel_converseN = "srel_converse";
+val srel_monoN = "srel_mono"
+val srel_ON = "srel_comp";
+val srel_O_GrN = "srel_comp_Gr";
 val set_naturalN = "set_natural";
 val set_natural'N = "set_natural'";
 val set_bdN = "set_bd";
@@ -736,28 +736,28 @@
 
     val pred = mk_bnf_pred QTs CA' CB';
 
-    val rel_rhs =
+    val srel_rhs =
       fold_rev Term.absfree Rs' (HOLogic.Collect_const CA'CB' $
         Term.lambda p (Term.list_comb (pred, map (mk_predicate_of_set (fst x') (fst y')) Rs) $
         HOLogic.mk_fst p $ HOLogic.mk_snd p));
 
-    val rel_bind_def = (fn () => Binding.suffix_name ("_" ^ relN) b, rel_rhs);
+    val srel_bind_def = (fn () => Binding.suffix_name ("_" ^ srelN) b, srel_rhs);
 
-    val ((bnf_rel_term, raw_rel_def), (lthy, lthy_old)) =
+    val ((bnf_srel_term, raw_srel_def), (lthy, lthy_old)) =
       lthy
-      |> maybe_define false rel_bind_def
+      |> maybe_define false srel_bind_def
       ||> `(maybe_restore lthy);
 
     val phi = Proof_Context.export_morphism lthy_old lthy;
-    val bnf_rel_def = Morphism.thm phi raw_rel_def;
-    val bnf_rel = Morphism.term phi bnf_rel_term;
+    val bnf_srel_def = Morphism.thm phi raw_srel_def;
+    val bnf_srel = Morphism.term phi bnf_srel_term;
 
-    fun mk_bnf_rel setRTs CA' CB' = normalize_rel lthy setRTs CA' CB' bnf_rel;
+    fun mk_bnf_srel setRTs CA' CB' = normalize_srel lthy setRTs CA' CB' bnf_srel;
 
-    val rel = mk_bnf_rel setRTs CA' CB';
+    val srel = mk_bnf_srel setRTs CA' CB';
 
     val _ = case no_reflexive (raw_map_def :: raw_set_defs @ [raw_bd_def] @
-        raw_wit_defs @ [raw_pred_def, raw_rel_def]) of
+        raw_wit_defs @ [raw_pred_def, raw_srel_def]) of
         [] => ()
       | defs => Proof_Display.print_consts true lthy_old (K false)
           (map (dest_Free o fst o Logic.dest_equals o prop_of) defs);
@@ -854,10 +854,10 @@
           (Logic.list_implies (prems, HOLogic.mk_Trueprop map_wpull))
       end;
 
-    val rel_O_Gr_goal = fold_rev Logic.all Rs (mk_Trueprop_eq (Term.list_comb (rel, Rs), O_Gr));
+    val srel_O_Gr_goal = fold_rev Logic.all Rs (mk_Trueprop_eq (Term.list_comb (srel, Rs), O_Gr));
 
     val goals = zip_axioms map_id_goal map_comp_goal map_cong_goal set_naturals_goal
-      card_order_bd_goal cinfinite_bd_goal set_bds_goal in_bd_goal map_wpull_goal rel_O_Gr_goal;
+      card_order_bd_goal cinfinite_bd_goal set_bds_goal in_bd_goal map_wpull_goal srel_O_Gr_goal;
 
     fun mk_wit_goals (I, wit) =
       let
@@ -978,43 +978,43 @@
             |> Thm.close_derivation
           end;
 
-        val rel_O_Grs = no_refl [#rel_O_Gr axioms];
+        val srel_O_Grs = no_refl [#srel_O_Gr axioms];
 
         val map_wppull = mk_lazy mk_map_wppull;
 
-        fun mk_rel_Gr () =
+        fun mk_srel_Gr () =
           let
-            val lhs = Term.list_comb (rel, map2 mk_Gr As fs);
+            val lhs = Term.list_comb (srel, map2 mk_Gr As fs);
             val rhs = mk_Gr (mk_in As bnf_sets_As CA') (Term.list_comb (bnf_map_AsBs, fs));
             val goal = fold_rev Logic.all (As @ fs) (mk_Trueprop_eq (lhs, rhs));
           in
             Skip_Proof.prove lthy [] [] goal
-              (mk_rel_Gr_tac rel_O_Grs (#map_id axioms) (#map_cong axioms) (Lazy.force map_id')
+              (mk_srel_Gr_tac srel_O_Grs (#map_id axioms) (#map_cong axioms) (Lazy.force map_id')
                 (Lazy.force map_comp') (map Lazy.force set_natural'))
             |> Thm.close_derivation
           end;
 
-        val rel_Gr = mk_lazy mk_rel_Gr;
+        val srel_Gr = mk_lazy mk_srel_Gr;
 
-        fun mk_rel_prems f = map2 (HOLogic.mk_Trueprop oo f) Rs Rs_copy
-        fun mk_rel_concl f = HOLogic.mk_Trueprop
-          (f (Term.list_comb (rel, Rs), Term.list_comb (rel, Rs_copy)));
+        fun mk_srel_prems f = map2 (HOLogic.mk_Trueprop oo f) Rs Rs_copy
+        fun mk_srel_concl f = HOLogic.mk_Trueprop
+          (f (Term.list_comb (srel, Rs), Term.list_comb (srel, Rs_copy)));
 
-        fun mk_rel_mono () =
+        fun mk_srel_mono () =
           let
-            val mono_prems = mk_rel_prems mk_subset;
-            val mono_concl = mk_rel_concl (uncurry mk_subset);
+            val mono_prems = mk_srel_prems mk_subset;
+            val mono_concl = mk_srel_concl (uncurry mk_subset);
           in
             Skip_Proof.prove lthy [] []
               (fold_rev Logic.all (Rs @ Rs_copy) (Logic.list_implies (mono_prems, mono_concl)))
-              (mk_rel_mono_tac rel_O_Grs (Lazy.force in_mono))
+              (mk_srel_mono_tac srel_O_Grs (Lazy.force in_mono))
             |> Thm.close_derivation
           end;
 
-        fun mk_rel_cong () =
+        fun mk_srel_cong () =
           let
-            val cong_prems = mk_rel_prems (curry HOLogic.mk_eq);
-            val cong_concl = mk_rel_concl HOLogic.mk_eq;
+            val cong_prems = mk_srel_prems (curry HOLogic.mk_eq);
+            val cong_concl = mk_srel_concl HOLogic.mk_eq;
           in
             Skip_Proof.prove lthy [] []
               (fold_rev Logic.all (Rs @ Rs_copy) (Logic.list_implies (cong_prems, cong_concl)))
@@ -1022,89 +1022,89 @@
             |> Thm.close_derivation
           end;
 
-        val rel_mono = mk_lazy mk_rel_mono;
-        val rel_cong = mk_lazy mk_rel_cong;
+        val srel_mono = mk_lazy mk_srel_mono;
+        val srel_cong = mk_lazy mk_srel_cong;
 
-        fun mk_rel_Id () =
-          let val relAsAs = mk_bnf_rel self_setRTs CA' CA' in
+        fun mk_srel_Id () =
+          let val relAsAs = 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')))
-              (mk_rel_Id_tac live (Lazy.force rel_Gr) (#map_id axioms))
+              (mk_srel_Id_tac live (Lazy.force srel_Gr) (#map_id axioms))
             |> Thm.close_derivation
           end;
 
-        val rel_Id = mk_lazy mk_rel_Id;
+        val srel_Id = mk_lazy mk_srel_Id;
 
-        fun mk_rel_converse () =
+        fun mk_srel_converse () =
           let
-            val relBsAs = mk_bnf_rel setRT's CB' CA';
+            val relBsAs = mk_bnf_srel setRT's CB' CA';
             val lhs = Term.list_comb (relBsAs, map mk_converse Rs);
-            val rhs = mk_converse (Term.list_comb (rel, 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
-              (mk_rel_converse_le_tac rel_O_Grs (Lazy.force rel_Id) (#map_cong axioms)
+              (mk_srel_converse_le_tac srel_O_Grs (Lazy.force srel_Id) (#map_cong axioms)
                 (Lazy.force map_comp') (map Lazy.force set_natural'))
               |> Thm.close_derivation
             val goal = fold_rev Logic.all Rs (mk_Trueprop_eq (lhs, rhs));
           in
-            Skip_Proof.prove lthy [] [] goal (fn _ => mk_rel_converse_tac le_thm)
+            Skip_Proof.prove lthy [] [] goal (fn _ => mk_srel_converse_tac le_thm)
             |> Thm.close_derivation
           end;
 
-        val rel_converse = mk_lazy mk_rel_converse;
+        val srel_converse = mk_lazy mk_srel_converse;
 
-        fun mk_rel_O () =
+        fun mk_srel_O () =
           let
-            val relAsCs = mk_bnf_rel setRTsAsCs CA' CC';
-            val relBsCs = mk_bnf_rel setRTsBsCs CB' CC';
+            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 (rel, Rs), Term.list_comb (relBsCs, Ss));
+            val rhs = mk_rel_comp (Term.list_comb (srel, Rs), Term.list_comb (relBsCs, Ss));
             val goal = fold_rev Logic.all (Rs @ Ss) (mk_Trueprop_eq (lhs, rhs));
           in
             Skip_Proof.prove lthy [] [] goal
-              (mk_rel_O_tac rel_O_Grs (Lazy.force rel_Id) (#map_cong axioms)
+              (mk_srel_O_tac srel_O_Grs (Lazy.force srel_Id) (#map_cong axioms)
                 (Lazy.force map_wppull) (Lazy.force map_comp') (map Lazy.force set_natural'))
             |> Thm.close_derivation
           end;
 
-        val rel_O = mk_lazy mk_rel_O;
+        val srel_O = mk_lazy mk_srel_O;
 
-        fun mk_in_rel () =
+        fun mk_in_srel () =
           let
             val bnf_in = mk_in Rs (map (mk_bnf_t RTs) bnf_sets) CRs';
             val map1 = Term.list_comb (mk_bnf_map RTs As', map fst_const RTs);
             val map2 = Term.list_comb (mk_bnf_map RTs Bs', map snd_const RTs);
             val map_fst_eq = HOLogic.mk_eq (map1 $ z, x);
             val map_snd_eq = HOLogic.mk_eq (map2 $ z, y);
-            val lhs = HOLogic.mk_mem (HOLogic.mk_prod (x, y), Term.list_comb (rel, Rs));
+            val lhs = HOLogic.mk_mem (HOLogic.mk_prod (x, y), Term.list_comb (srel, Rs));
             val rhs =
               HOLogic.mk_exists (fst z', snd z', HOLogic.mk_conj (HOLogic.mk_mem (z, bnf_in),
                 HOLogic.mk_conj (map_fst_eq, map_snd_eq)));
             val goal =
               fold_rev Logic.all (x :: y :: Rs) (mk_Trueprop_eq (lhs, rhs));
           in
-            Skip_Proof.prove lthy [] [] goal (mk_in_rel_tac rel_O_Grs (length bnf_sets))
+            Skip_Proof.prove lthy [] [] goal (mk_in_srel_tac srel_O_Grs (length bnf_sets))
             |> Thm.close_derivation
           end;
 
-        val in_rel = mk_lazy mk_in_rel;
+        val in_srel = mk_lazy mk_in_srel;
 
-        val defs = mk_defs bnf_map_def bnf_set_defs bnf_pred_def bnf_rel_def;
+        val defs = mk_defs bnf_map_def bnf_set_defs bnf_pred_def bnf_srel_def;
 
-        val facts = mk_facts bd_Card_order bd_Cinfinite bd_Cnotzero collect_set_natural
-          in_cong in_mono in_rel map_comp' map_id' map_wppull
-          rel_cong rel_mono rel_Id rel_Gr rel_converse rel_O set_natural';
+        val facts = mk_facts bd_Card_order bd_Cinfinite bd_Cnotzero collect_set_natural in_cong
+          in_mono in_srel map_comp' map_id' map_wppull set_natural' srel_cong srel_mono srel_Id
+          srel_Gr srel_converse srel_O;
 
         val wits = map2 mk_witness bnf_wits wit_thms;
 
-        val bnf_pred = Term.subst_atomic_types
-          ((Ds ~~ deads) @ (As' ~~ alphas) @ (Bs' ~~ betas)) pred;
-        val bnf_rel = Term.subst_atomic_types
-          ((Ds ~~ deads) @ (As' ~~ alphas) @ (Bs' ~~ betas)) rel;
+        val bnf_pred =
+          Term.subst_atomic_types ((Ds ~~ deads) @ (As' ~~ alphas) @ (Bs' ~~ betas)) pred;
+        val bnf_srel =
+          Term.subst_atomic_types ((Ds ~~ deads) @ (As' ~~ alphas) @ (Bs' ~~ betas)) srel;
 
         val bnf = mk_bnf b CA live alphas betas dead deads bnf_map bnf_sets bnf_bd axioms defs facts
-          wits bnf_pred bnf_rel;
+          wits bnf_pred bnf_srel;
       in
         (bnf, lthy
           |> (if fact_policy = Note_All_Facts_and_Axioms then
@@ -1119,7 +1119,7 @@
                     (collect_set_naturalN, [Lazy.force (#collect_set_natural facts)]),
                     (in_bdN, [#in_bd axioms]),
                     (in_monoN, [Lazy.force (#in_mono facts)]),
-                    (in_relN, [Lazy.force (#in_rel facts)]),
+                    (in_srelN, [Lazy.force (#in_srel facts)]),
                     (map_compN, [#map_comp axioms]),
                     (map_idN, [#map_id axioms]),
                     (map_wpullN, [#map_wpull axioms]),
@@ -1138,16 +1138,16 @@
                  fact_policy = Derive_All_Facts_Note_Most then
                 let
                   val notes =
-                    [(map_congN, [#map_cong axioms]),
-                    (rel_O_GrN, rel_O_Grs),
-                    (rel_IdN, [Lazy.force (#rel_Id facts)]),
-                    (rel_GrN, [Lazy.force (#rel_Gr facts)]),
-                    (rel_converseN, [Lazy.force (#rel_converse facts)]),
-                    (rel_monoN, [Lazy.force (#rel_mono facts)]),
-                    (rel_ON, [Lazy.force (#rel_O facts)]),
+                    [(map_comp'N, [Lazy.force (#map_comp' facts)]),
+                    (map_congN, [#map_cong axioms]),
                     (map_id'N, [Lazy.force (#map_id' facts)]),
-                    (map_comp'N, [Lazy.force (#map_comp' facts)]),
-                    (set_natural'N, map Lazy.force (#set_natural' facts))]
+                    (set_natural'N, map Lazy.force (#set_natural' facts)),
+                    (srel_O_GrN, srel_O_Grs),
+                    (srel_IdN, [Lazy.force (#srel_Id facts)]),
+                    (srel_GrN, [Lazy.force (#srel_Gr facts)]),
+                    (srel_converseN, [Lazy.force (#srel_converse facts)]),
+                    (srel_monoN, [Lazy.force (#srel_mono facts)]),
+                    (srel_ON, [Lazy.force (#srel_O facts)])]
                     |> filter_out (null o #2)
                     |> map (fn (thmN, thms) =>
                       ((qualify (Binding.qualify true (Binding.name_of b) (Binding.name thmN)), []),
@@ -1161,7 +1161,7 @@
 
     val one_step_defs =
       no_reflexive (bnf_map_def :: bnf_bd_def :: bnf_set_defs @ bnf_wit_defs @ [bnf_pred_def,
-        bnf_rel_def]);
+        bnf_srel_def]);
   in
     (key, goals, wit_goalss, after_qed, lthy, one_step_defs)
   end;
diff -r a944eefb67e6 -r aeb0cc8889f2 src/HOL/Codatatype/Tools/bnf_def_tactics.ML
--- a/src/HOL/Codatatype/Tools/bnf_def_tactics.ML	Fri Sep 21 15:53:29 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_def_tactics.ML	Fri Sep 21 15:53:29 2012 +0200
@@ -15,16 +15,16 @@
   val mk_map_wppull_tac: thm -> thm -> thm -> thm -> thm list -> tactic
   val mk_set_natural': thm -> thm
 
-  val mk_rel_Gr_tac: thm list -> thm -> thm -> thm -> thm -> thm list ->
+  val mk_srel_Gr_tac: thm list -> thm -> thm -> thm -> thm -> thm list ->
     {prems: thm list, context: Proof.context} -> tactic
-  val mk_rel_Id_tac: int -> thm -> thm -> {prems: 'a, context: Proof.context} -> tactic
-  val mk_rel_O_tac: thm list -> thm -> thm -> thm -> thm -> thm list ->
+  val mk_srel_Id_tac: int -> thm -> thm -> {prems: 'a, context: Proof.context} -> tactic
+  val mk_srel_O_tac: thm list -> thm -> thm -> thm -> thm -> thm list ->
     {prems: thm list, context: Proof.context} -> tactic
-  val mk_in_rel_tac: thm list -> int -> {prems: 'b, context: Proof.context} -> tactic
-  val mk_rel_converse_tac: thm -> tactic
-  val mk_rel_converse_le_tac: thm list -> thm -> thm -> thm -> thm list ->
+  val mk_in_srel_tac: thm list -> int -> {prems: 'b, context: Proof.context} -> tactic
+  val mk_srel_converse_tac: thm -> tactic
+  val mk_srel_converse_le_tac: thm list -> thm -> thm -> thm -> thm list ->
     {prems: thm list, context: Proof.context} -> tactic
-  val mk_rel_mono_tac: thm list -> thm -> {prems: 'a, context: Proof.context} -> tactic
+  val mk_srel_mono_tac: thm list -> thm -> {prems: 'a, context: Proof.context} -> tactic
 end;
 
 structure BNF_Def_Tactics : BNF_DEF_TACTICS =
@@ -63,14 +63,14 @@
         rtac (o_apply RS trans RS sym), rtac (o_apply RS trans), rtac thm,
         rtac conjunct2, etac bspec, etac set_mp, atac]]) [conjunct1, conjunct2]] 1;
 
-fun mk_rel_Gr_tac rel_O_Grs map_id map_cong map_id' map_comp set_naturals
+fun mk_srel_Gr_tac srel_O_Grs map_id map_cong map_id' map_comp set_naturals
   {context = ctxt, prems = _} =
   let
     val n = length set_naturals;
   in
     if null set_naturals then
-      unfold_thms_tac ctxt rel_O_Grs THEN EVERY' [rtac @{thm Gr_UNIV_id}, rtac map_id] 1
-    else unfold_thms_tac ctxt (@{thm Gr_def} :: rel_O_Grs) THEN
+      unfold_thms_tac ctxt srel_O_Grs THEN EVERY' [rtac @{thm Gr_UNIV_id}, rtac map_id] 1
+    else unfold_thms_tac ctxt (@{thm Gr_def} :: srel_O_Grs) THEN
       EVERY' [rtac equalityI, rtac subsetI,
         REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE, @{thm relcompE}, @{thm converseE}],
         REPEAT_DETERM o dtac Pair_eqD,
@@ -104,28 +104,28 @@
           @{thms fst_convol snd_convol} [map_id', refl])] 1
   end;
 
-fun mk_rel_Id_tac n rel_Gr map_id {context = ctxt, prems = _} =
-  unfold_thms_tac ctxt [rel_Gr, @{thm Id_alt}] THEN
+fun mk_srel_Id_tac n srel_Gr map_id {context = ctxt, prems = _} =
+  unfold_thms_tac ctxt [srel_Gr, @{thm Id_alt}] THEN
   subst_tac ctxt [map_id] 1 THEN
     (if n = 0 then rtac refl 1
     else EVERY' [rtac @{thm arg_cong2[of _ _ _ _ Gr]},
       rtac equalityI, rtac subset_UNIV, rtac subsetI, rtac CollectI,
       CONJ_WRAP' (K (rtac subset_UNIV)) (1 upto n), rtac refl] 1);
 
-fun mk_rel_mono_tac rel_O_Grs in_mono {context = ctxt, prems = _} =
-  unfold_thms_tac ctxt rel_O_Grs THEN
+fun mk_srel_mono_tac srel_O_Grs in_mono {context = ctxt, prems = _} =
+  unfold_thms_tac ctxt srel_O_Grs THEN
     EVERY' [rtac @{thm relcomp_mono}, rtac @{thm iffD2[OF converse_mono]},
       rtac @{thm Gr_mono}, rtac in_mono, REPEAT_DETERM o atac,
       rtac @{thm Gr_mono}, rtac in_mono, REPEAT_DETERM o atac] 1;
 
-fun mk_rel_converse_le_tac rel_O_Grs rel_Id map_cong map_comp set_naturals
+fun mk_srel_converse_le_tac srel_O_Grs srel_Id map_cong map_comp set_naturals
   {context = ctxt, prems = _} =
   let
     val n = length set_naturals;
   in
     if null set_naturals then
-      unfold_thms_tac ctxt [rel_Id] THEN rtac equalityD2 1 THEN rtac @{thm converse_Id} 1
-    else unfold_thms_tac ctxt (@{thm Gr_def} :: rel_O_Grs) THEN
+      unfold_thms_tac ctxt [srel_Id] THEN rtac equalityD2 1 THEN rtac @{thm converse_Id} 1
+    else unfold_thms_tac ctxt (@{thm Gr_def} :: srel_O_Grs) THEN
       EVERY' [rtac @{thm subrelI},
         REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE, @{thm relcompE}, @{thm converseE}],
         REPEAT_DETERM o dtac Pair_eqD,
@@ -139,11 +139,11 @@
             etac @{thm flip_rel}]) set_naturals]) [@{thm snd_fst_flip}, @{thm fst_snd_flip}])] 1
   end;
 
-fun mk_rel_converse_tac le_converse =
+fun mk_srel_converse_tac le_converse =
   EVERY' [rtac equalityI, rtac le_converse, rtac @{thm xt1(6)}, rtac @{thm converse_shift},
     rtac le_converse, REPEAT_DETERM o stac @{thm converse_converse}, rtac subset_refl] 1;
 
-fun mk_rel_O_tac rel_O_Grs rel_Id map_cong map_wppull map_comp set_naturals
+fun mk_srel_O_tac srel_O_Grs srel_Id map_cong map_wppull map_comp set_naturals
   {context = ctxt, prems = _} =
   let
     val n = length set_naturals;
@@ -151,8 +151,8 @@
         CONJ_WRAP' (fn thm => EVERY' [rtac (thm RS @{thm ord_eq_le_trans}),
           rtac @{thm image_subsetI}, rtac nthO_in, etac set_mp, atac]) set_naturals;
   in
-    if null set_naturals then unfold_thms_tac ctxt [rel_Id] THEN rtac (@{thm Id_O_R} RS sym) 1
-    else unfold_thms_tac ctxt (@{thm Gr_def} :: rel_O_Grs) THEN
+    if null set_naturals then unfold_thms_tac ctxt [srel_Id] THEN rtac (@{thm Id_O_R} RS sym) 1
+    else unfold_thms_tac ctxt (@{thm Gr_def} :: srel_O_Grs) THEN
       EVERY' [rtac equalityI, rtac @{thm subrelI},
         REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE, @{thm relcompE}, @{thm converseE}],
         REPEAT_DETERM o dtac Pair_eqD,
@@ -193,11 +193,11 @@
           rtac (map_comp RS sym), atac, atac]) [@{thm fst_fstO}, @{thm snd_sndO}])] 1
   end;
 
-fun mk_in_rel_tac rel_O_Grs m {context = ctxt, prems = _} =
+fun mk_in_srel_tac srel_O_Grs m {context = ctxt, prems = _} =
   let
     val ls' = replicate (Int.max (1, m)) ();
   in
-    unfold_thms_tac ctxt (rel_O_Grs @
+    unfold_thms_tac ctxt (srel_O_Grs @
       @{thms Gr_def converse_unfold relcomp_unfold mem_Collect_eq prod.cases Pair_eq}) THEN
     EVERY' [rtac iffI, REPEAT_DETERM o eresolve_tac [exE, conjE], hyp_subst_tac, rtac exI,
       rtac conjI, CONJ_WRAP' (K atac) ls', rtac conjI, rtac refl, rtac refl,
diff -r a944eefb67e6 -r aeb0cc8889f2 src/HOL/Codatatype/Tools/bnf_fp.ML
--- a/src/HOL/Codatatype/Tools/bnf_fp.ML	Fri Sep 21 15:53:29 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_fp.ML	Fri Sep 21 15:53:29 2012 +0200
@@ -67,15 +67,15 @@
   val pred_strong_coinductN: string
   val recN: string
   val recsN: string
-  val rel_coinductN: string
-  val rel_simpN: string
-  val rel_strong_coinductN: string
   val rvN: string
   val sel_unfoldsN: string
   val sel_corecsN: string
   val set_inclN: string
   val set_set_inclN: string
   val simpsN: string
+  val srel_coinductN: string
+  val srel_simpN: string
+  val srel_strong_coinductN: string
   val strTN: string
   val str_initN: string
   val strongN: string
@@ -222,15 +222,15 @@
 val ctor_inductN = ctorN ^ "_" ^ inductN
 val ctor_induct2N = ctor_inductN ^ "2"
 val dtor_coinductN = dtorN ^ "_" ^ coinductN
-val rel_coinductN = relN ^ "_" ^ coinductN
 val pred_coinductN = predN ^ "_" ^ coinductN
+val srel_coinductN = srelN ^ "_" ^ coinductN
 val simpN = "_simp";
-val rel_simpN = relN ^ simpN;
+val srel_simpN = srelN ^ simpN;
 val pred_simpN = predN ^ simpN;
 val strongN = "strong_"
 val dtor_strong_coinductN = dtorN ^ "_" ^ strongN ^ coinductN
-val rel_strong_coinductN = relN ^ "_" ^ strongN ^ coinductN
 val pred_strong_coinductN = predN ^ "_" ^ strongN ^ coinductN
+val srel_strong_coinductN = srelN ^ "_" ^ strongN ^ coinductN
 val hsetN = "Hset"
 val hset_recN = hsetN ^ "_rec"
 val set_inclN = "set_incl"
diff -r a944eefb67e6 -r aeb0cc8889f2 src/HOL/Codatatype/Tools/bnf_gfp.ML
--- a/src/HOL/Codatatype/Tools/bnf_gfp.ML	Fri Sep 21 15:53:29 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_gfp.ML	Fri Sep 21 15:53:29 2012 +0200
@@ -144,7 +144,7 @@
     val setssAs = mk_setss allAs;
     val setssAs' = transpose setssAs;
     val bis_setss = mk_setss (passiveAs @ RTs);
-    val relsAsBs = map4 mk_rel_of_bnf Dss Ass Bss bnfs;
+    val relsAsBs = map4 mk_srel_of_bnf Dss Ass Bss bnfs;
     val bds = map3 mk_bd_of_bnf Dss Ass bnfs;
     val sum_bd = Library.foldr1 (uncurry mk_csum) bds;
     val sum_bdT = fst (dest_relT (fastype_of sum_bd));
@@ -220,17 +220,17 @@
     val map_comp's = map map_comp'_of_bnf bnfs;
     val map_congs = map map_cong_of_bnf bnfs;
     val map_id's = map map_id'_of_bnf bnfs;
-    val rel_congs = map rel_cong_of_bnf bnfs;
-    val rel_converses = map rel_converse_of_bnf bnfs;
-    val rel_defs = map rel_def_of_bnf bnfs;
-    val rel_Grs = map rel_Gr_of_bnf bnfs;
-    val rel_Ids = map rel_Id_of_bnf bnfs;
-    val rel_monos = map rel_mono_of_bnf bnfs;
-    val rel_Os = map rel_O_of_bnf bnfs;
-    val rel_O_Grs = map rel_O_Gr_of_bnf bnfs;
     val map_wpulls = map map_wpull_of_bnf bnfs;
     val set_bdss = map set_bd_of_bnf bnfs;
     val set_natural'ss = map set_natural'_of_bnf bnfs;
+    val srel_congs = map srel_cong_of_bnf bnfs;
+    val srel_converses = map srel_converse_of_bnf bnfs;
+    val srel_defs = map srel_def_of_bnf bnfs;
+    val srel_Grs = map srel_Gr_of_bnf bnfs;
+    val srel_Ids = map srel_Id_of_bnf bnfs;
+    val srel_monos = map srel_mono_of_bnf bnfs;
+    val srel_Os = map srel_O_of_bnf bnfs;
+    val srel_O_Grs = map srel_O_Gr_of_bnf bnfs;
 
     val timer = time (timer "Extracted terms & thms");
 
@@ -846,13 +846,13 @@
         |> Thm.close_derivation
       end;
 
-    val bis_rel_thm =
+    val bis_srel_thm =
       let
-        fun mk_conjunct R s s' b1 b2 rel =
+        fun mk_conjunct R s s' b1 b2 srel =
           list_all_free [b1, b2] (HOLogic.mk_imp
             (HOLogic.mk_mem (HOLogic.mk_prod (b1, b2), R),
             HOLogic.mk_mem (HOLogic.mk_prod (s $ b1, s' $ b2),
-              Term.list_comb (rel, passive_diags @ Rs))));
+              Term.list_comb (srel, passive_diags @ Rs))));
 
         val rhs = HOLogic.mk_conj
           (bis_le, Library.foldr1 HOLogic.mk_conj
@@ -861,7 +861,7 @@
         Skip_Proof.prove lthy [] []
           (fold_rev Logic.all (As @ Bs @ ss @ B's @ s's @ Rs)
             (mk_Trueprop_eq (mk_bis As Bs ss B's s's Rs, rhs)))
-          (K (mk_bis_rel_tac m bis_def rel_O_Grs map_comp's map_congs set_natural'ss))
+          (K (mk_bis_srel_tac m bis_def srel_O_Grs map_comp's map_congs set_natural'ss))
         |> Thm.close_derivation
       end;
 
@@ -871,7 +871,7 @@
           (Logic.mk_implies
             (HOLogic.mk_Trueprop (mk_bis As Bs ss B's s's Rs),
             HOLogic.mk_Trueprop (mk_bis As B's s's Bs ss (map mk_converse Rs)))))
-        (K (mk_bis_converse_tac m bis_rel_thm rel_congs rel_converses))
+        (K (mk_bis_converse_tac m bis_srel_thm srel_congs srel_converses))
       |> Thm.close_derivation;
 
     val bis_O_thm =
@@ -885,7 +885,7 @@
         Skip_Proof.prove lthy [] []
           (fold_rev Logic.all (As @ Bs @ ss @ B's @ s's @ B''s @ s''s @ Rs @ R's)
             (Logic.list_implies (prems, concl)))
-          (K (mk_bis_O_tac m bis_rel_thm rel_congs rel_Os))
+          (K (mk_bis_O_tac m bis_srel_thm srel_congs srel_Os))
         |> Thm.close_derivation
       end;
 
@@ -897,7 +897,7 @@
         Skip_Proof.prove lthy [] []
           (fold_rev Logic.all (As @ Bs @ ss @ B's @ s's @ fs)
             (Logic.list_implies ([coalg_prem, mor_prem], concl)))
-          (mk_bis_Gr_tac bis_rel_thm rel_Grs mor_image_thms morE_thms coalg_in_thms)
+          (mk_bis_Gr_tac bis_srel_thm srel_Grs mor_image_thms morE_thms coalg_in_thms)
         |> Thm.close_derivation
       end;
 
@@ -2178,8 +2178,8 @@
 
     val timer = time (timer "corec definitions & thms");
 
-    val (dtor_coinduct_thm, coinduct_params, rel_coinduct_thm, pred_coinduct_thm,
-         dtor_strong_coinduct_thm, rel_strong_coinduct_thm, pred_strong_coinduct_thm) =
+    val (dtor_coinduct_thm, coinduct_params, srel_coinduct_thm, pred_coinduct_thm,
+         dtor_strong_coinduct_thm, srel_strong_coinduct_thm, pred_strong_coinduct_thm) =
       let
         val zs = Jzs1 @ Jzs2;
         val frees = phis @ zs;
@@ -2191,34 +2191,34 @@
             (HOLogic.mk_disj (phi $ z1 $ z2, HOLogic.mk_eq (z1, z2))))
           else phi;
 
-        fun phi_rels upto_eq = map4 (fn phi => fn T => fn z1 => fn z2 =>
+        fun phi_srels upto_eq = map4 (fn phi => fn T => fn z1 => fn z2 =>
           HOLogic.Collect_const (HOLogic.mk_prodT (T, T)) $
             HOLogic.mk_split (mk_phi upto_eq phi z1 z2)) phis Ts Jzs1 Jzs2;
 
-        val rels = map (Term.subst_atomic_types ((activeAs ~~ Ts) @ (activeBs ~~ Ts))) relsAsBs;
+        val srels = map (Term.subst_atomic_types ((activeAs ~~ Ts) @ (activeBs ~~ Ts))) relsAsBs;
 
         fun mk_concl phi z1 z2 = HOLogic.mk_imp (phi $ z1 $ z2, HOLogic.mk_eq (z1, z2));
         val concl = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
           (map3 mk_concl phis Jzs1 Jzs2));
 
-        fun mk_rel_prem upto_eq phi dtor rel Jz Jz_copy =
+        fun mk_srel_prem upto_eq phi dtor srel Jz Jz_copy =
           let
             val concl = HOLogic.mk_mem (HOLogic.mk_tuple [dtor $ Jz, dtor $ Jz_copy],
-              Term.list_comb (rel, mk_Ids upto_eq @ phi_rels upto_eq));
+              Term.list_comb (srel, mk_Ids upto_eq @ phi_srels upto_eq));
           in
             HOLogic.mk_Trueprop
               (list_all_free [Jz, Jz_copy] (HOLogic.mk_imp (phi $ Jz $ Jz_copy, concl)))
           end;
 
-        val rel_prems = map5 (mk_rel_prem false) phis dtors rels Jzs Jzs_copy;
-        val rel_upto_prems = map5 (mk_rel_prem true) phis dtors rels Jzs Jzs_copy;
-
-        val rel_coinduct_goal = fold_rev Logic.all frees (Logic.list_implies (rel_prems, concl));
-        val coinduct_params = rev (Term.add_tfrees rel_coinduct_goal []);
-
-        val rel_coinduct = unfold_thms lthy @{thms diag_UNIV}
-          (Skip_Proof.prove lthy [] [] rel_coinduct_goal
-            (K (mk_rel_coinduct_tac ks raw_coind_thm bis_rel_thm))
+        val srel_prems = map5 (mk_srel_prem false) phis dtors srels Jzs Jzs_copy;
+        val srel_upto_prems = map5 (mk_srel_prem true) phis dtors srels Jzs Jzs_copy;
+
+        val srel_coinduct_goal = fold_rev Logic.all frees (Logic.list_implies (srel_prems, concl));
+        val coinduct_params = rev (Term.add_tfrees srel_coinduct_goal []);
+
+        val srel_coinduct = unfold_thms lthy @{thms diag_UNIV}
+          (Skip_Proof.prove lthy [] [] srel_coinduct_goal
+            (K (mk_srel_coinduct_tac ks raw_coind_thm bis_srel_thm))
           |> Thm.close_derivation);
 
         fun mk_dtor_prem upto_eq phi dtor map_nth sets Jz Jz_copy FJz =
@@ -2256,10 +2256,10 @@
         val cTs = map (SOME o certifyT lthy o TFree) coinduct_params;
         val cts = map3 (SOME o certify lthy ooo mk_phi true) phis Jzs1 Jzs2;
 
-        val rel_strong_coinduct = singleton (Proof_Context.export names_lthy lthy)
+        val srel_strong_coinduct = singleton (Proof_Context.export names_lthy lthy)
           (Skip_Proof.prove lthy [] []
-            (fold_rev Logic.all zs (Logic.list_implies (rel_upto_prems, concl)))
-            (K (mk_rel_strong_coinduct_tac m cTs cts rel_coinduct rel_monos rel_Ids)))
+            (fold_rev Logic.all zs (Logic.list_implies (srel_upto_prems, concl)))
+            (K (mk_srel_strong_coinduct_tac m cTs cts srel_coinduct srel_monos srel_Ids)))
           |> Thm.close_derivation;
 
         val dtor_strong_coinduct = singleton (Proof_Context.export names_lthy lthy)
@@ -2269,14 +2269,14 @@
               (tcoalg_thm RS bis_diag_thm))))
           |> Thm.close_derivation;
 
-        val pred_of_rel_thms =
-          rel_defs @ @{thms Id_def' mem_Collect_eq fst_conv snd_conv split_conv};
-
-        val pred_coinduct = unfold_thms lthy pred_of_rel_thms rel_coinduct;
-        val pred_strong_coinduct = unfold_thms lthy pred_of_rel_thms rel_strong_coinduct;
+        val pred_of_srel_thms =
+          srel_defs @ @{thms Id_def' mem_Collect_eq fst_conv snd_conv split_conv};
+
+        val pred_coinduct = unfold_thms lthy pred_of_srel_thms srel_coinduct;
+        val pred_strong_coinduct = unfold_thms lthy pred_of_srel_thms srel_strong_coinduct;
       in
-        (dtor_coinduct, rev (Term.add_tfrees dtor_coinduct_goal []), rel_coinduct, pred_coinduct,
-         dtor_strong_coinduct, rel_strong_coinduct, pred_strong_coinduct)
+        (dtor_coinduct, rev (Term.add_tfrees dtor_coinduct_goal []), srel_coinduct, pred_coinduct,
+         dtor_strong_coinduct, srel_strong_coinduct, pred_strong_coinduct)
       end;
 
     val timer = time (timer "coinduction");
@@ -2672,10 +2672,10 @@
           map3 (K ooo mk_wpull_tac m coalg_thePull_thm mor_thePull_fst_thm mor_thePull_snd_thm
             mor_thePull_pick_thm) unique_mor_thms (transpose pick_col_thmss) hset_defss;
 
-        val rel_O_Gr_tacs = replicate n (simple_rel_O_Gr_tac o #context);
+        val srel_O_Gr_tacs = replicate n (simple_srel_O_Gr_tac o #context);
 
         val tacss = map10 zip_axioms map_id_tacs map_comp_tacs map_cong_tacs set_nat_tacss
-          bd_co_tacs bd_cinf_tacs set_bd_tacss in_bd_tacs map_wpull_tacs rel_O_Gr_tacs;
+          bd_co_tacs bd_cinf_tacs set_bd_tacss in_bd_tacs map_wpull_tacs srel_O_Gr_tacs;
 
         val (hset_dtor_incl_thmss, hset_hset_dtor_incl_thmsss, hset_induct_thms) =
           let
@@ -2880,40 +2880,40 @@
         val set_set_incl_thmsss = map (map (map fold_sets)) hset_hset_dtor_incl_thmsss;
         val set_induct_thms = map fold_sets hset_induct_thms;
 
-        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 srels = map2 (fn Ds => mk_srel_of_bnf Ds (passiveAs @ Ts) (passiveBs @ Ts')) Dss bnfs;
+        val Jsrels = map (mk_srel_of_bnf deads passiveAs passiveBs) Jbnfs;
         val preds = map2 (fn Ds => mk_pred_of_bnf Ds (passiveAs @ Ts) (passiveBs @ Ts')) Dss bnfs;
         val Jpreds = map (mk_pred_of_bnf deads passiveAs passiveBs) Jbnfs;
 
-        val JrelRs = map (fn Jrel => Term.list_comb (Jrel, JRs)) Jrels;
-        val relRs = map (fn rel => Term.list_comb (rel, JRs @ JrelRs)) rels;
-        val Jpredphis = map (fn Jrel => Term.list_comb (Jrel, Jphis)) Jpreds;
-        val predphis = map (fn rel => Term.list_comb (rel, Jphis @ Jpredphis)) preds;
-
-        val in_rels = map in_rel_of_bnf bnfs;
-        val in_Jrels = map in_rel_of_bnf Jbnfs;
-        val Jrel_defs = map rel_def_of_bnf 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)) Jpreds;
+        val predphis = map (fn srel => Term.list_comb (srel, Jphis @ Jpredphis)) preds;
+
+        val in_srels = map in_srel_of_bnf bnfs;
+        val in_Jsrels = map in_srel_of_bnf Jbnfs;
+        val Jsrel_defs = map srel_def_of_bnf Jbnfs;
         val Jpred_defs = map pred_def_of_bnf Jbnfs;
 
         val folded_map_simp_thms = map fold_maps map_simp_thms;
         val folded_set_simp_thmss = map (map fold_sets) set_simp_thmss;
         val folded_set_simp_thmss' = transpose folded_set_simp_thmss;
 
-        val Jrel_simp_thms =
+        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;
           in
-            map12 (fn i => fn goal => fn in_rel => fn map_comp => fn map_cong =>
+            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 =>
               fn set_naturals => fn set_incls => fn set_set_inclss =>
               Skip_Proof.prove lthy [] [] goal
-                (K (mk_rel_simp_tac in_Jrels i in_rel map_comp map_cong map_simp set_simps
+                (K (mk_srel_simp_tac in_Jsrels i in_srel map_comp map_cong map_simp set_simps
                   dtor_inject dtor_ctor set_naturals set_incls set_set_inclss))
               |> Thm.close_derivation)
-            ks goals in_rels map_comp's map_congs folded_map_simp_thms folded_set_simp_thmss'
+            ks goals in_srels map_comp's map_congs folded_map_simp_thms folded_set_simp_thmss'
               dtor_inject_thms dtor_ctor_thms set_natural'ss set_incl_thmss set_set_incl_thmsss
           end;
 
@@ -2923,11 +2923,11 @@
               (mk_Trueprop_eq (Jpredphi $ Jz $ Jz', predphi $ (dtor $ Jz) $ (dtor' $ Jz')));
             val goals = map6 mk_goal Jzs Jz's dtors dtor's Jpredphis predphis;
           in
-            map3 (fn goal => fn rel_def => fn Jrel_simp =>
+            map3 (fn goal => fn srel_def => fn Jsrel_simp =>
               Skip_Proof.prove lthy [] [] goal
-                (mk_pred_simp_tac rel_def Jpred_defs Jrel_defs Jrel_simp)
+                (mk_pred_simp_tac srel_def Jpred_defs Jsrel_defs Jsrel_simp)
               |> Thm.close_derivation)
-            goals rel_defs Jrel_simp_thms
+            goals srel_defs Jsrel_simp_thms
           end;
 
         val timer = time (timer "additional properties");
@@ -2942,10 +2942,10 @@
 
         val Jbnf_notes =
           [(map_simpsN, map single folded_map_simp_thms),
+          (pred_simpN, map single Jpred_simp_thms),
           (set_inclN, set_incl_thmss),
           (set_set_inclN, map flat set_set_incl_thmsss),
-          (rel_simpN, map single Jrel_simp_thms),
-          (pred_simpN, map single Jpred_simp_thms)] @
+          (srel_simpN, map single Jsrel_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 =>
@@ -2957,11 +2957,11 @@
 
       val common_notes =
         [(dtor_coinductN, [dtor_coinduct_thm]),
-        (rel_coinductN, [rel_coinduct_thm]),
+        (dtor_strong_coinductN, [dtor_strong_coinduct_thm]),
         (pred_coinductN, [pred_coinduct_thm]),
-        (dtor_strong_coinductN, [dtor_strong_coinduct_thm]),
-        (rel_strong_coinductN, [rel_strong_coinduct_thm]),
-        (pred_strong_coinductN, [pred_strong_coinduct_thm])]
+        (pred_strong_coinductN, [pred_strong_coinduct_thm]),
+        (srel_coinductN, [srel_coinduct_thm]),
+        (srel_strong_coinductN, [srel_strong_coinduct_thm])]
         |> map (fn (thmN, thms) =>
           ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])]));
 
diff -r a944eefb67e6 -r aeb0cc8889f2 src/HOL/Codatatype/Tools/bnf_gfp_tactics.ML
--- a/src/HOL/Codatatype/Tools/bnf_gfp_tactics.ML	Fri Sep 21 15:53:29 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_gfp_tactics.ML	Fri Sep 21 15:53:29 2012 +0200
@@ -17,7 +17,7 @@
   val mk_bis_O_tac: int -> thm -> thm list -> thm list -> tactic
   val mk_bis_Union_tac: thm -> thm list -> {prems: 'a, context: Proof.context} -> tactic
   val mk_bis_converse_tac: int -> thm -> thm list -> thm list -> tactic
-  val mk_bis_rel_tac: int -> thm -> thm list -> thm list -> thm list -> thm list list -> tactic
+  val mk_bis_srel_tac: int -> thm -> thm list -> thm list -> thm list -> thm list list -> tactic
   val mk_carT_set_tac: int -> int -> thm -> thm -> thm -> thm ->
     {prems: 'a, context: Proof.context} -> tactic
   val mk_card_of_carT_tac: int -> thm list -> thm -> thm -> thm -> thm -> thm -> thm list -> tactic
@@ -38,8 +38,8 @@
   val mk_corec_tac: int -> thm list -> thm -> thm -> thm list ->
     {prems: 'a, context: Proof.context} -> tactic
   val mk_dtor_coinduct_tac: int -> int list -> thm -> thm -> tactic
-  val mk_dtor_strong_coinduct_tac: int list -> ctyp option list -> cterm option list -> thm -> thm ->
-    thm -> tactic
+  val mk_dtor_strong_coinduct_tac: int list -> ctyp option list -> cterm option list -> thm ->
+    thm -> thm -> tactic
   val mk_dtor_o_ctor_tac: thm -> thm -> thm -> thm -> thm list ->
     {prems: 'a, context: Proof.context} -> tactic
   val mk_equiv_lsbis_tac: thm -> thm -> thm -> thm -> thm -> thm -> tactic
@@ -91,11 +91,6 @@
     tactic
   val mk_raw_coind_tac: thm -> thm -> thm -> thm -> thm -> thm -> thm -> thm -> thm -> thm list ->
     thm list -> thm list -> thm -> thm list -> tactic
-  val mk_rel_coinduct_tac: 'a list -> thm -> thm -> tactic
-  val mk_rel_strong_coinduct_tac: int -> ctyp option list -> cterm option list -> thm -> thm list ->
-    thm list -> tactic
-  val mk_rel_simp_tac: thm list -> int -> thm -> thm -> thm -> thm -> thm list -> thm -> thm ->
-    thm list -> thm list -> thm list list -> tactic
   val mk_rv_last_tac: ctyp option list -> cterm option list -> thm list -> thm list -> tactic
   val mk_sbis_lsbis_tac: thm list -> thm -> thm -> tactic
   val mk_set_Lev_tac: cterm option list -> thm list -> thm list -> thm list -> thm list ->
@@ -111,6 +106,11 @@
   val mk_set_rv_Lev_tac: int -> cterm option list -> thm list -> thm list -> thm list -> thm list ->
     thm list list -> thm list list -> tactic
   val mk_set_simp_tac: int -> thm -> thm -> thm list -> tactic
+  val mk_srel_coinduct_tac: 'a list -> thm -> thm -> tactic
+  val mk_srel_strong_coinduct_tac: int -> ctyp option list -> cterm option list -> thm ->
+    thm list -> thm list -> tactic
+  val mk_srel_simp_tac: thm list -> int -> thm -> thm -> thm -> thm -> thm list -> thm -> thm ->
+    thm list -> thm list -> thm list list -> tactic
   val mk_strT_hset_tac: int -> int -> int -> ctyp option list -> ctyp option list ->
     cterm option list -> thm list -> thm list -> thm list -> thm list -> thm list list ->
     thm list list -> thm list list -> thm -> thm list list -> tactic
@@ -256,15 +256,15 @@
   EVERY' [rtac (hset_def RS trans), rtac (refl RS @{thm UN_cong} RS trans), etac mor_hset_rec,
     atac, atac, rtac (hset_def RS sym)] 1
 
-fun mk_bis_rel_tac m bis_def rel_O_Grs map_comps map_congs set_naturalss =
+fun mk_bis_srel_tac m bis_def srel_O_Grs map_comps map_congs set_naturalss =
   let
-    val n = length rel_O_Grs;
-    val thms = ((1 upto n) ~~ map_comps ~~ map_congs ~~ set_naturalss ~~ rel_O_Grs);
+    val n = length srel_O_Grs;
+    val thms = ((1 upto n) ~~ map_comps ~~ map_congs ~~ set_naturalss ~~ srel_O_Grs);
 
-    fun mk_if_tac ((((i, map_comp), map_cong), set_naturals), rel_O_Gr) =
+    fun mk_if_tac ((((i, map_comp), map_cong), set_naturals), srel_O_Gr) =
       EVERY' [rtac allI, rtac allI, rtac impI, dtac (mk_conjunctN n i),
         etac allE, etac allE, etac impE, atac, etac bexE, etac conjE,
-        rtac (rel_O_Gr RS equalityD2 RS set_mp),
+        rtac (srel_O_Gr RS equalityD2 RS set_mp),
         rtac @{thm relcompI}, rtac @{thm converseI},
         EVERY' (map (fn thm =>
           EVERY' [rtac @{thm GrI}, REPEAT_DETERM o eresolve_tac [CollectE, conjE],
@@ -280,10 +280,10 @@
             REPEAT_DETERM_N n o rtac (@{thm o_id} RS fun_cong), atac])
           @{thms fst_diag_id snd_diag_id})];
 
-    fun mk_only_if_tac ((((i, map_comp), map_cong), set_naturals), rel_O_Gr) =
+    fun mk_only_if_tac ((((i, map_comp), map_cong), set_naturals), srel_O_Gr) =
       EVERY' [dtac (mk_conjunctN n i), rtac allI, rtac allI, rtac impI,
         etac allE, etac allE, etac impE, atac,
-        dtac (rel_O_Gr RS equalityD1 RS set_mp),
+        dtac (srel_O_Gr RS equalityD1 RS set_mp),
         REPEAT_DETERM o eresolve_tac [CollectE, @{thm relcompE}, @{thm converseE}],
         REPEAT_DETERM o eresolve_tac [@{thm GrE}, exE, conjE],
         REPEAT_DETERM o dtac Pair_eqD,
@@ -313,39 +313,39 @@
       etac conjE, etac conjI, CONJ_WRAP' mk_only_if_tac thms] 1
   end;
 
-fun mk_bis_converse_tac m bis_rel rel_congs rel_converses =
-  EVERY' [stac bis_rel, dtac (bis_rel RS iffD1),
+fun mk_bis_converse_tac m bis_srel srel_congs srel_converses =
+  EVERY' [stac bis_srel, dtac (bis_srel RS iffD1),
     REPEAT_DETERM o etac conjE, rtac conjI,
     CONJ_WRAP' (K (EVERY' [rtac @{thm converse_shift}, etac subset_trans,
-      rtac equalityD2, rtac @{thm converse_Times}])) rel_congs,
-    CONJ_WRAP' (fn (rel_cong, rel_converse) =>
+      rtac equalityD2, rtac @{thm converse_Times}])) srel_congs,
+    CONJ_WRAP' (fn (srel_cong, srel_converse) =>
       EVERY' [rtac allI, rtac allI, rtac impI, rtac @{thm set_mp[OF equalityD2]},
-        rtac (rel_cong RS trans),
+        rtac (srel_cong RS trans),
         REPEAT_DETERM_N m o rtac @{thm diag_converse},
-        REPEAT_DETERM_N (length rel_congs) o rtac refl,
-        rtac rel_converse,
+        REPEAT_DETERM_N (length srel_congs) o rtac refl,
+        rtac srel_converse,
         REPEAT_DETERM o etac allE,
-        rtac @{thm converseI}, etac mp, etac @{thm converseD}]) (rel_congs ~~ rel_converses)] 1;
+        rtac @{thm converseI}, etac mp, etac @{thm converseD}]) (srel_congs ~~ srel_converses)] 1;
 
-fun mk_bis_O_tac m bis_rel rel_congs rel_Os =
-  EVERY' [stac bis_rel, REPEAT_DETERM o dtac (bis_rel RS iffD1),
+fun mk_bis_O_tac m bis_srel srel_congs srel_Os =
+  EVERY' [stac bis_srel, REPEAT_DETERM o dtac (bis_srel RS iffD1),
     REPEAT_DETERM o etac conjE, rtac conjI,
-    CONJ_WRAP' (K (EVERY' [etac @{thm relcomp_subset_Sigma}, atac])) rel_congs,
-    CONJ_WRAP' (fn (rel_cong, rel_O) =>
+    CONJ_WRAP' (K (EVERY' [etac @{thm relcomp_subset_Sigma}, atac])) srel_congs,
+    CONJ_WRAP' (fn (srel_cong, srel_O) =>
       EVERY' [rtac allI, rtac allI, rtac impI, rtac @{thm set_mp[OF equalityD2]},
-        rtac (rel_cong RS trans),
+        rtac (srel_cong RS trans),
         REPEAT_DETERM_N m o rtac @{thm diag_Comp},
-        REPEAT_DETERM_N (length rel_congs) o rtac refl,
-        rtac rel_O,
+        REPEAT_DETERM_N (length srel_congs) o rtac refl,
+        rtac srel_O,
         etac @{thm relcompE},
         REPEAT_DETERM o dtac Pair_eqD,
         etac conjE, hyp_subst_tac,
         REPEAT_DETERM o etac allE, rtac @{thm relcompI},
-        etac mp, atac, etac mp, atac]) (rel_congs ~~ rel_Os)] 1;
+        etac mp, atac, etac mp, atac]) (srel_congs ~~ srel_Os)] 1;
 
-fun mk_bis_Gr_tac bis_rel rel_Grs mor_images morEs coalg_ins
+fun mk_bis_Gr_tac bis_srel srel_Grs mor_images morEs coalg_ins
   {context = ctxt, prems = _} =
-  unfold_thms_tac ctxt (bis_rel :: @{thm diag_Gr} :: rel_Grs) THEN
+  unfold_thms_tac ctxt (bis_srel :: @{thm diag_Gr} :: srel_Grs) THEN
   EVERY' [rtac conjI,
     CONJ_WRAP' (fn thm => rtac (@{thm Gr_incl} RS ssubst) THEN' etac thm) mor_images,
     CONJ_WRAP' (fn (coalg_in, morE) =>
@@ -1123,8 +1123,8 @@
     REPEAT_DETERM_N m o rtac refl,
     EVERY' (map (fn thm => rtac @{thm sum_case_expand_Inr} THEN' rtac thm) corec_Inls)] 1;
 
-fun mk_rel_coinduct_tac ks raw_coind bis_rel =
-  EVERY' [rtac rev_mp, rtac raw_coind, rtac ssubst, rtac bis_rel, rtac conjI,
+fun mk_srel_coinduct_tac ks raw_coind bis_srel =
+  EVERY' [rtac rev_mp, rtac raw_coind, rtac ssubst, rtac bis_srel, rtac conjI,
     CONJ_WRAP' (K (rtac @{thm ord_le_eq_trans[OF subset_UNIV UNIV_Times_UNIV[THEN sym]]})) ks,
     CONJ_WRAP' (K (EVERY' [rtac allI, rtac allI, rtac impI,
       REPEAT_DETERM o etac allE, etac mp, etac CollectE, etac @{thm splitD}])) ks,
@@ -1132,17 +1132,17 @@
     CONJ_WRAP' (K (EVERY' [rtac impI, rtac @{thm IdD}, etac set_mp,
       rtac CollectI, etac @{thm prod_caseI}])) ks] 1;
 
-fun mk_rel_strong_coinduct_tac m cTs cts rel_coinduct rel_monos rel_Ids =
-  EVERY' [rtac rev_mp, rtac (Drule.instantiate' cTs cts rel_coinduct),
-    EVERY' (map2 (fn rel_mono => fn rel_Id =>
+fun mk_srel_strong_coinduct_tac m cTs cts srel_coinduct srel_monos srel_Ids =
+  EVERY' [rtac rev_mp, rtac (Drule.instantiate' cTs cts srel_coinduct),
+    EVERY' (map2 (fn srel_mono => fn srel_Id =>
       EVERY' [REPEAT_DETERM o resolve_tac [allI, impI], REPEAT_DETERM o etac allE,
-        etac disjE, etac mp, atac, hyp_subst_tac, rtac (rel_mono RS set_mp),
+        etac disjE, etac mp, atac, hyp_subst_tac, rtac (srel_mono RS set_mp),
         REPEAT_DETERM_N m o rtac @{thm subset_refl},
-        REPEAT_DETERM_N (length rel_monos) o rtac @{thm Id_subset},
-        rtac (rel_Id RS equalityD2 RS set_mp), rtac @{thm IdI}])
-    rel_monos rel_Ids),
+        REPEAT_DETERM_N (length srel_monos) o rtac @{thm Id_subset},
+        rtac (srel_Id RS equalityD2 RS set_mp), rtac @{thm IdI}])
+    srel_monos srel_Ids),
     rtac impI, REPEAT_DETERM o etac conjE,
-    CONJ_WRAP' (K (rtac impI THEN' etac mp THEN' etac disjI1)) rel_Ids] 1;
+    CONJ_WRAP' (K (rtac impI THEN' etac mp THEN' etac disjI1)) srel_Ids] 1;
 
 fun mk_dtor_coinduct_tac m ks raw_coind bis_def =
   let
@@ -1494,27 +1494,27 @@
   ALLGOALS (TRY o
     FIRST' [rtac TrueI, rtac refl, etac (refl RSN (2, mp)), dresolve_tac wits THEN' etac FalseE])
 
-fun mk_rel_simp_tac in_Jrels i in_rel map_comp map_cong map_simp set_simps dtor_inject dtor_ctor
+fun mk_srel_simp_tac in_Jsrels i in_srel map_comp map_cong map_simp set_simps dtor_inject dtor_ctor
   set_naturals set_incls set_set_inclss =
   let
     val m = length set_incls;
     val n = length set_set_inclss;
     val (passive_set_naturals, active_set_naturals) = chop m set_naturals;
-    val in_Jrel = nth in_Jrels (i - 1);
+    val in_Jsrel = nth in_Jsrels (i - 1);
     val if_tac =
-      EVERY' [dtac (in_Jrel RS iffD1), REPEAT_DETERM o eresolve_tac [exE, conjE, CollectE],
-        rtac (in_rel RS iffD2), rtac exI, rtac conjI, rtac CollectI,
+      EVERY' [dtac (in_Jsrel RS iffD1), REPEAT_DETERM o eresolve_tac [exE, conjE, CollectE],
+        rtac (in_srel RS iffD2), rtac exI, rtac conjI, rtac CollectI,
         EVERY' (map2 (fn set_natural => fn set_incl =>
           EVERY' [rtac conjI, rtac ord_eq_le_trans, rtac set_natural,
             rtac ord_eq_le_trans, rtac trans_fun_cong_image_id_id_apply,
             etac (set_incl RS @{thm subset_trans})])
         passive_set_naturals set_incls),
-        CONJ_WRAP' (fn (in_Jrel, (set_natural, set_set_incls)) =>
+        CONJ_WRAP' (fn (in_Jsrel, (set_natural, set_set_incls)) =>
           EVERY' [rtac ord_eq_le_trans, rtac set_natural, rtac @{thm image_subsetI},
-            rtac (in_Jrel RS iffD2), rtac exI, rtac conjI, rtac CollectI,
+            rtac (in_Jsrel RS iffD2), rtac exI, rtac conjI, rtac CollectI,
             CONJ_WRAP' (fn thm => etac (thm RS @{thm subset_trans}) THEN' atac) set_set_incls,
             rtac conjI, rtac refl, rtac refl])
-        (in_Jrels ~~ (active_set_naturals ~~ set_set_inclss)),
+        (in_Jsrels ~~ (active_set_naturals ~~ set_set_inclss)),
         CONJ_WRAP' (fn conv =>
           EVERY' [rtac trans, rtac map_comp, rtac trans, rtac map_cong,
           REPEAT_DETERM_N m o rtac @{thm fun_cong[OF o_id]},
@@ -1522,30 +1522,30 @@
           rtac trans, rtac sym, rtac map_simp, rtac (dtor_inject RS iffD2), atac])
         @{thms fst_conv snd_conv}];
     val only_if_tac =
-      EVERY' [dtac (in_rel RS iffD1), REPEAT_DETERM o eresolve_tac [exE, conjE, CollectE],
-        rtac (in_Jrel RS iffD2), rtac exI, rtac conjI, rtac CollectI,
+      EVERY' [dtac (in_srel RS iffD1), REPEAT_DETERM o eresolve_tac [exE, conjE, CollectE],
+        rtac (in_Jsrel RS iffD2), rtac exI, rtac conjI, rtac CollectI,
         CONJ_WRAP' (fn (set_simp, passive_set_natural) =>
           EVERY' [rtac ord_eq_le_trans, rtac set_simp, rtac @{thm Un_least},
             rtac ord_eq_le_trans, rtac box_equals, rtac passive_set_natural,
             rtac (dtor_ctor RS sym RS arg_cong), rtac trans_fun_cong_image_id_id_apply, atac,
             CONJ_WRAP_GEN' (rtac (Thm.permute_prems 0 1 @{thm Un_least}))
-              (fn (active_set_natural, in_Jrel) => EVERY' [rtac ord_eq_le_trans,
+              (fn (active_set_natural, in_Jsrel) => EVERY' [rtac ord_eq_le_trans,
                 rtac @{thm UN_cong[OF _ refl]}, rtac @{thm box_equals[OF _ _ refl]},
                 rtac active_set_natural, rtac (dtor_ctor RS sym RS arg_cong), rtac @{thm UN_least},
                 dtac set_rev_mp, etac @{thm image_mono}, etac imageE,
-                dtac @{thm ssubst_mem[OF pair_collapse]}, dtac (in_Jrel RS iffD1),
+                dtac @{thm ssubst_mem[OF pair_collapse]}, dtac (in_Jsrel RS iffD1),
                 dtac @{thm someI_ex}, REPEAT_DETERM o etac conjE,
                 dtac (Thm.permute_prems 0 1 @{thm ssubst_mem}), atac,
                 hyp_subst_tac, REPEAT_DETERM o eresolve_tac [CollectE, conjE], atac])
-            (rev (active_set_naturals ~~ in_Jrels))])
+            (rev (active_set_naturals ~~ in_Jsrels))])
         (set_simps ~~ passive_set_naturals),
         rtac conjI,
         REPEAT_DETERM_N 2 o EVERY'[rtac (dtor_inject RS iffD1), rtac trans, rtac map_simp,
           rtac box_equals, rtac map_comp, rtac (dtor_ctor RS sym RS arg_cong), rtac trans,
           rtac map_cong, REPEAT_DETERM_N m o rtac @{thm fun_cong[OF o_id]},
-          EVERY' (map (fn in_Jrel => EVERY' [rtac trans, rtac o_apply, dtac set_rev_mp, atac,
-            dtac @{thm ssubst_mem[OF pair_collapse]}, dtac (in_Jrel RS iffD1), dtac @{thm someI_ex},
-            REPEAT_DETERM o etac conjE, atac]) in_Jrels),
+          EVERY' (map (fn in_Jsrel => EVERY' [rtac trans, rtac o_apply, dtac set_rev_mp, atac,
+            dtac @{thm ssubst_mem[OF pair_collapse]}, dtac (in_Jsrel RS iffD1),
+            dtac @{thm someI_ex}, REPEAT_DETERM o etac conjE, atac]) in_Jsrels),
           atac]]
   in
     EVERY' [rtac iffI, if_tac, only_if_tac] 1
diff -r a944eefb67e6 -r aeb0cc8889f2 src/HOL/Codatatype/Tools/bnf_lfp.ML
--- a/src/HOL/Codatatype/Tools/bnf_lfp.ML	Fri Sep 21 15:53:29 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_lfp.ML	Fri Sep 21 15:53:29 2012 +0200
@@ -1671,10 +1671,10 @@
           in_incl_min_alg_thms card_of_min_alg_thms;
         val map_wpull_tacs = map (K o mk_wpull_tac) map_wpull_thms;
 
-        val rel_O_Gr_tacs = replicate n (simple_rel_O_Gr_tac o #context);
+        val srel_O_Gr_tacs = replicate n (simple_srel_O_Gr_tac o #context);
 
         val tacss = map10 zip_axioms map_id_tacs map_comp_tacs map_cong_tacs set_nat_tacss
-          bd_co_tacs bd_cinf_tacs set_bd_tacss in_bd_tacs map_wpull_tacs rel_O_Gr_tacs;
+          bd_co_tacs bd_cinf_tacs set_bd_tacss in_bd_tacs map_wpull_tacs srel_O_Gr_tacs;
 
         val ctor_witss =
           let
@@ -1720,20 +1720,20 @@
 
         val timer = time (timer "registered new datatypes as BNFs");
 
-        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 srels = map2 (fn Ds => mk_srel_of_bnf Ds (passiveAs @ Ts) (passiveBs @ Ts')) Dss bnfs;
+        val Isrels = map (mk_srel_of_bnf deads passiveAs passiveBs) Ibnfs;
         val preds = map2 (fn Ds => mk_pred_of_bnf Ds (passiveAs @ Ts) (passiveBs @ Ts')) Dss bnfs;
         val Ipreds = map (mk_pred_of_bnf deads passiveAs passiveBs) Ibnfs;
 
-        val IrelRs = map (fn Irel => Term.list_comb (Irel, IRs)) Irels;
-        val relRs = map (fn rel => Term.list_comb (rel, IRs @ IrelRs)) rels;
-        val Ipredphis = map (fn Irel => Term.list_comb (Irel, Iphis)) Ipreds;
-        val predphis = map (fn rel => Term.list_comb (rel, Iphis @ Ipredphis)) preds;
+        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)) Ipreds;
+        val predphis = map (fn srel => Term.list_comb (srel, Iphis @ Ipredphis)) preds;
 
-        val in_rels = map in_rel_of_bnf bnfs;
-        val in_Irels = map in_rel_of_bnf Ibnfs;
-        val rel_defs = map rel_def_of_bnf bnfs;
-        val Irel_defs = map rel_def_of_bnf Ibnfs;
+        val in_srels = map in_srel_of_bnf bnfs;
+        val in_Isrels = map in_srel_of_bnf Ibnfs;
+        val srel_defs = map srel_def_of_bnf bnfs;
+        val Isrel_defs = map srel_def_of_bnf Ibnfs;
         val Ipred_defs = map pred_def_of_bnf Ibnfs;
 
         val set_incl_thmss = map (map (fold_sets o hd)) Fset_set_thmsss;
@@ -1742,21 +1742,21 @@
         val folded_set_simp_thmss = map (map fold_sets) set_simp_thmss;
         val folded_set_simp_thmss' = transpose folded_set_simp_thmss;
 
-        val Irel_simp_thms =
+        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;
           in
-            map12 (fn i => fn goal => fn in_rel => fn map_comp => fn map_cong =>
+            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 =>
               fn set_naturals => fn set_incls => fn set_set_inclss =>
               Skip_Proof.prove lthy [] [] goal
-               (K (mk_rel_simp_tac in_Irels i in_rel map_comp map_cong map_simp set_simps
+               (K (mk_srel_simp_tac in_Isrels i in_srel map_comp map_cong map_simp set_simps
                  ctor_inject ctor_dtor set_naturals set_incls set_set_inclss))
               |> Thm.close_derivation)
-            ks goals in_rels map_comp's map_congs folded_map_simp_thms folded_set_simp_thmss'
+            ks goals in_srels map_comp's map_congs folded_map_simp_thms folded_set_simp_thmss'
               ctor_inject_thms ctor_dtor_thms set_natural'ss set_incl_thmss set_set_incl_thmsss
           end;
 
@@ -1766,11 +1766,11 @@
               (mk_Trueprop_eq (Ipredphi $ (ctor $ xF) $ (ctor' $ yF), predphi $ xF $ yF));
             val goals = map6 mk_goal xFs yFs ctors ctor's Ipredphis predphis;
           in
-            map3 (fn goal => fn rel_def => fn Irel_simp =>
+            map3 (fn goal => fn srel_def => fn Isrel_simp =>
               Skip_Proof.prove lthy [] [] goal
-                (mk_pred_simp_tac rel_def Ipred_defs Irel_defs Irel_simp)
+                (mk_pred_simp_tac srel_def Ipred_defs Isrel_defs Isrel_simp)
               |> Thm.close_derivation)
-            goals rel_defs Irel_simp_thms
+            goals srel_defs Isrel_simp_thms
           end;
 
         val timer = time (timer "additional properties");
@@ -1786,7 +1786,7 @@
           [(map_simpsN, map single folded_map_simp_thms),
           (set_inclN, set_incl_thmss),
           (set_set_inclN, map flat set_set_incl_thmsss),
-          (rel_simpN, map single Irel_simp_thms),
+          (srel_simpN, map single Isrel_simp_thms),
           (pred_simpN, map single Ipred_simp_thms)] @
           map2 (fn i => fn thms => (mk_set_simpsN i, map single thms)) ls' folded_set_simp_thmss
           |> maps (fn (thmN, thmss) =>
diff -r a944eefb67e6 -r aeb0cc8889f2 src/HOL/Codatatype/Tools/bnf_lfp_tactics.ML
--- a/src/HOL/Codatatype/Tools/bnf_lfp_tactics.ML	Fri Sep 21 15:53:29 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_lfp_tactics.ML	Fri Sep 21 15:53:29 2012 +0200
@@ -22,6 +22,7 @@
     thm list -> tactic
   val mk_ctor_induct2_tac: ctyp option list -> cterm option list -> thm -> thm list ->
     {prems: 'a, context: Proof.context} -> tactic
+  val mk_dtor_o_ctor_tac: thm -> thm -> thm -> thm -> thm list -> tactic
   val mk_ex_copy_alg_tac: int -> thm -> thm -> tactic
   val mk_in_bd_tac: thm -> thm -> thm -> thm -> tactic
   val mk_incl_min_alg_tac: (int -> tactic) -> thm list list list -> thm list -> thm ->
@@ -61,8 +62,6 @@
     thm list -> tactic
   val mk_mor_str_tac: 'a list -> thm -> tactic
   val mk_rec_tac: thm list -> thm -> thm list -> {prems: 'a, context: Proof.context} -> tactic
-  val mk_rel_simp_tac: thm list -> int -> thm -> thm -> thm -> thm -> thm list -> thm ->
-    thm -> thm list -> thm list -> thm list list -> tactic
   val mk_set_bd_tac: int -> (int -> tactic) -> thm -> thm list list -> thm list -> int ->
     {prems: 'a, context: Proof.context} -> tactic
   val mk_set_nat_tac: int -> (int -> tactic) -> thm list list -> thm list -> cterm list ->
@@ -70,7 +69,8 @@
   val mk_set_natural_tac: thm -> tactic
   val mk_set_simp_tac: thm -> thm -> thm list -> tactic
   val mk_set_tac: thm -> tactic
-  val mk_dtor_o_ctor_tac: thm -> thm -> thm -> thm -> thm list -> tactic
+  val mk_srel_simp_tac: thm list -> int -> thm -> thm -> thm -> thm -> thm list -> thm ->
+    thm -> thm list -> thm list -> thm list list -> tactic
   val mk_wit_tac: int -> thm list -> thm list -> tactic
   val mk_wpull_tac: thm -> tactic
 end;
@@ -770,32 +770,32 @@
           EVERY' [hyp_subst_tac, dtac set_rev_mp, rtac equalityD1, resolve_tac set_simp,
             REPEAT_DETERM_N n o etac UnE]))))] 1);
 
-fun mk_rel_simp_tac in_Irels i in_rel map_comp map_cong map_simp set_simps ctor_inject
+fun mk_srel_simp_tac in_Isrels i in_srel map_comp map_cong map_simp set_simps ctor_inject
   ctor_dtor set_naturals set_incls set_set_inclss =
   let
     val m = length set_incls;
     val n = length set_set_inclss;
 
     val (passive_set_naturals, active_set_naturals) = chop m set_naturals;
-    val in_Irel = nth in_Irels (i - 1);
+    val in_Isrel = nth in_Isrels (i - 1);
     val le_arg_cong_ctor_dtor = ctor_dtor RS arg_cong RS ord_eq_le_trans;
     val eq_arg_cong_ctor_dtor = ctor_dtor RS arg_cong RS trans;
     val if_tac =
-      EVERY' [dtac (in_Irel RS iffD1), REPEAT_DETERM o eresolve_tac [exE, conjE, CollectE],
-        rtac (in_rel RS iffD2), rtac exI, rtac conjI, rtac CollectI,
+      EVERY' [dtac (in_Isrel RS iffD1), REPEAT_DETERM o eresolve_tac [exE, conjE, CollectE],
+        rtac (in_srel RS iffD2), rtac exI, rtac conjI, rtac CollectI,
         EVERY' (map2 (fn set_natural => fn set_incl =>
           EVERY' [rtac conjI, rtac ord_eq_le_trans, rtac set_natural,
             rtac ord_eq_le_trans, rtac trans_fun_cong_image_id_id_apply,
             rtac (set_incl RS subset_trans), etac le_arg_cong_ctor_dtor])
         passive_set_naturals set_incls),
-        CONJ_WRAP' (fn (in_Irel, (set_natural, set_set_incls)) =>
+        CONJ_WRAP' (fn (in_Isrel, (set_natural, set_set_incls)) =>
           EVERY' [rtac ord_eq_le_trans, rtac set_natural, rtac @{thm image_subsetI},
-            rtac (in_Irel RS iffD2), rtac exI, rtac conjI, rtac CollectI,
+            rtac (in_Isrel RS iffD2), rtac exI, rtac conjI, rtac CollectI,
             CONJ_WRAP' (fn thm =>
               EVERY' (map etac [thm RS subset_trans, le_arg_cong_ctor_dtor]))
             set_set_incls,
             rtac conjI, rtac refl, rtac refl])
-        (in_Irels ~~ (active_set_naturals ~~ set_set_inclss)),
+        (in_Isrels ~~ (active_set_naturals ~~ set_set_inclss)),
         CONJ_WRAP' (fn conv =>
           EVERY' [rtac trans, rtac map_comp, rtac trans, rtac map_cong,
           REPEAT_DETERM_N m o rtac @{thm fun_cong[OF o_id]},
@@ -804,29 +804,29 @@
           etac eq_arg_cong_ctor_dtor])
         fst_snd_convs];
     val only_if_tac =
-      EVERY' [dtac (in_rel RS iffD1), REPEAT_DETERM o eresolve_tac [exE, conjE, CollectE],
-        rtac (in_Irel RS iffD2), rtac exI, rtac conjI, rtac CollectI,
+      EVERY' [dtac (in_srel RS iffD1), REPEAT_DETERM o eresolve_tac [exE, conjE, CollectE],
+        rtac (in_Isrel RS iffD2), rtac exI, rtac conjI, rtac CollectI,
         CONJ_WRAP' (fn (set_simp, passive_set_natural) =>
           EVERY' [rtac ord_eq_le_trans, rtac set_simp, rtac @{thm Un_least},
             rtac ord_eq_le_trans, rtac @{thm box_equals[OF _ refl]},
             rtac passive_set_natural, rtac trans_fun_cong_image_id_id_apply, atac,
             CONJ_WRAP_GEN' (rtac (Thm.permute_prems 0 1 @{thm Un_least}))
-              (fn (active_set_natural, in_Irel) => EVERY' [rtac ord_eq_le_trans,
+              (fn (active_set_natural, in_Isrel) => EVERY' [rtac ord_eq_le_trans,
                 rtac @{thm UN_cong[OF _ refl]}, rtac active_set_natural, rtac @{thm UN_least},
                 dtac set_rev_mp, etac @{thm image_mono}, etac imageE,
-                dtac @{thm ssubst_mem[OF pair_collapse]}, dtac (in_Irel RS iffD1),
+                dtac @{thm ssubst_mem[OF pair_collapse]}, dtac (in_Isrel RS iffD1),
                 dtac @{thm someI_ex}, REPEAT_DETERM o etac conjE,
                 dtac (Thm.permute_prems 0 1 @{thm ssubst_mem}), atac,
                 hyp_subst_tac, REPEAT_DETERM o eresolve_tac [CollectE, conjE], atac])
-            (rev (active_set_naturals ~~ in_Irels))])
+            (rev (active_set_naturals ~~ in_Isrels))])
         (set_simps ~~ passive_set_naturals),
         rtac conjI,
         REPEAT_DETERM_N 2 o EVERY' [rtac trans, rtac map_simp, rtac (ctor_inject RS iffD2),
           rtac trans, rtac map_comp, rtac trans, rtac map_cong,
           REPEAT_DETERM_N m o rtac @{thm fun_cong[OF o_id]},
-          EVERY' (map (fn in_Irel => EVERY' [rtac trans, rtac o_apply, dtac set_rev_mp, atac,
-            dtac @{thm ssubst_mem[OF pair_collapse]}, dtac (in_Irel RS iffD1), dtac @{thm someI_ex},
-            REPEAT_DETERM o etac conjE, atac]) in_Irels),
+          EVERY' (map (fn in_Isrel => EVERY' [rtac trans, rtac o_apply, dtac set_rev_mp, atac,
+            dtac @{thm ssubst_mem[OF pair_collapse]}, dtac (in_Isrel RS iffD1),
+            dtac @{thm someI_ex}, REPEAT_DETERM o etac conjE, atac]) in_Isrels),
           atac]]
   in
     EVERY' [rtac iffI, if_tac, only_if_tac] 1
diff -r a944eefb67e6 -r aeb0cc8889f2 src/HOL/Codatatype/Tools/bnf_tactics.ML
--- a/src/HOL/Codatatype/Tools/bnf_tactics.ML	Fri Sep 21 15:53:29 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_tactics.ML	Fri Sep 21 15:53:29 2012 +0200
@@ -26,7 +26,7 @@
   val mk_Abs_bij_thm: Proof.context -> thm -> thm -> thm
   val mk_Abs_inj_thm: thm -> thm
 
-  val simple_rel_O_Gr_tac: Proof.context -> tactic
+  val simple_srel_O_Gr_tac: Proof.context -> tactic
   val mk_pred_simp_tac: thm -> thm list -> thm list -> thm -> {prems: 'a, context: Proof.context} ->
     tactic
 
@@ -98,14 +98,14 @@
     gen_tac
   end;
 
-fun simple_rel_O_Gr_tac ctxt =
+fun simple_srel_O_Gr_tac ctxt =
   unfold_thms_tac ctxt @{thms Collect_fst_snd_mem_eq Collect_pair_mem_eq} THEN rtac refl 1;
 
-fun mk_pred_simp_tac rel_def IJpred_defs IJrel_defs rel_simp {context = ctxt, prems = _} =
+fun mk_pred_simp_tac srel_def IJpred_defs IJsrel_defs srel_simp {context = ctxt, prems = _} =
   unfold_thms_tac ctxt IJpred_defs THEN
-  subst_tac ctxt [unfold_thms ctxt (IJpred_defs @ IJrel_defs @
-    @{thms Collect_pair_mem_eq mem_Collect_eq fst_conv snd_conv}) rel_simp] 1 THEN
-  unfold_thms_tac ctxt (rel_def ::
+  subst_tac ctxt [unfold_thms ctxt (IJpred_defs @ IJsrel_defs @
+    @{thms Collect_pair_mem_eq mem_Collect_eq fst_conv snd_conv}) srel_simp] 1 THEN
+  unfold_thms_tac ctxt (srel_def ::
     @{thms Collect_fst_snd_mem_eq mem_Collect_eq pair_mem_Collect_split fst_conv snd_conv
       split_conv}) THEN
   rtac refl 1;