renamed "dtor_rel_coinduct" etc. to "dtor_coinduct"

--- a/src/HOL/BNF/Examples/Infinite_Derivation_Trees/Tree.thy	Wed Sep 26 10:00:59 2012 +0200
+++ b/src/HOL/BNF/Examples/Infinite_Derivation_Trees/Tree.thy	Wed Sep 26 10:00:59 2012 +0200
@@ -130,7 +130,7 @@
           \<lbrakk>\<phi> (NNode n1 as1) (NNode n2 as2)\<rbrakk> \<Longrightarrow>
           n1 = n2 \<and> llift2 \<phi> as1 as2"
 shows "tr1 = tr2"
-apply(rule mp[OF Tree.dtor_rel_coinduct[of \<phi> tr1 tr2] phi]) proof clarify
+apply(rule mp[OF Tree.dtor_coinduct[of \<phi> tr1 tr2] phi]) proof clarify
   fix tr1 tr2  assume \<phi>: "\<phi> tr1 tr2"
   show "pre_Tree_rel \<phi> (Tree_dtor tr1) (Tree_dtor tr2)"
   apply(cases rule: Tree.ctor_exhaust[of tr1], cases rule: Tree.ctor_exhaust[of tr2])

--- a/src/HOL/BNF/Examples/Process.thy	Wed Sep 26 10:00:59 2012 +0200
+++ b/src/HOL/BNF/Examples/Process.thy	Wed Sep 26 10:00:59 2012 +0200
@@ -45,7 +45,7 @@
 Act: "\<And> a a' p p'. \<phi> (Action a p) (Action a' p') \<Longrightarrow> a = a' \<and> \<phi> p p'" and
 Ch: "\<And> p q p' q'. \<phi> (Choice p q) (Choice p' q') \<Longrightarrow> \<phi> p p' \<and> \<phi> q q'"
 shows "p = p'"
-proof(intro mp[OF process.dtor_rel_coinduct, of \<phi>, OF _ phi], clarify)
+proof(intro mp[OF process.dtor_coinduct, of \<phi>, OF _ phi], clarify)
   fix p p'  assume \<phi>: "\<phi> p p'"
   show "pre_process_rel (op =) \<phi> (process_dtor p) (process_dtor p')"
   proof(cases rule: process.exhaust[of p])

--- a/src/HOL/BNF/Examples/Stream.thy	Wed Sep 26 10:00:59 2012 +0200
+++ b/src/HOL/BNF/Examples/Stream.thy	Wed Sep 26 10:00:59 2012 +0200
@@ -122,7 +122,7 @@
 unfolding prod_rel_def by auto
 
 lemmas stream_coind =
-  mp[OF stream.dtor_rel_coinduct, unfolded prod_rel[abs_def], folded hdd_def tll_def]
+  mp[OF stream.dtor_coinduct, unfolded prod_rel[abs_def], folded hdd_def tll_def]
 
 definition plus :: "nat stream \<Rightarrow> nat stream \<Rightarrow> nat stream" (infixr "\<oplus>" 66) where
   [simp]: "plus xs ys =

--- a/src/HOL/BNF/Examples/TreeFsetI.thy	Wed Sep 26 10:00:59 2012 +0200
+++ b/src/HOL/BNF/Examples/TreeFsetI.thy	Wed Sep 26 10:00:59 2012 +0200
@@ -50,7 +50,7 @@
 apply (simp add: pre_treeFsetI_rel_def prod_rel_def fset_rel_def)
 done
 
-lemmas treeFsetI_coind = mp[OF treeFsetI.dtor_rel_coinduct]
+lemmas treeFsetI_coind = mp[OF treeFsetI.dtor_coinduct]
 
 lemma "tmap (f o g) x = tmap f (tmap g x)"
 by (intro treeFsetI_coind[where P="%x1 x2. \<exists>x. x1 = tmap (f o g) x \<and> x2 = tmap f (tmap g x)"])

--- a/src/HOL/BNF/Tools/bnf_fp.ML	Wed Sep 26 10:00:59 2012 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp.ML	Wed Sep 26 10:00:59 2012 +0200
@@ -44,6 +44,7 @@
   val disc_corec_iffN: string
   val disc_corecsN: string
   val dtorN: string
+  val dtor_coinductN: string
   val dtor_corecN: string
   val dtor_corecsN: string
   val dtor_ctorN: string
@@ -54,13 +55,12 @@
   val dtor_map_strong_coinductN: string
   val dtor_map_uniqueN: string
   val dtor_relN: string
-  val dtor_rel_coinductN: string
-  val dtor_rel_strong_coinductN: string
   val dtor_set_inclN: string
   val dtor_set_set_inclN: string
   val dtor_srelN: string
   val dtor_srel_coinductN: string
   val dtor_srel_strong_coinductN: string
+  val dtor_strong_coinductN: string
   val dtor_unfoldN: string
   val dtor_unfold_uniqueN: string
   val dtor_unfoldsN: string
@@ -244,11 +244,11 @@
 val ctor_inductN = ctorN ^ "_" ^ inductN
 val ctor_induct2N = ctor_inductN ^ "2"
 val dtor_map_coinductN = dtor_mapN ^ "_" ^ coinductN
-val dtor_rel_coinductN = dtor_relN ^ "_" ^ coinductN
+val dtor_coinductN = dtorN ^ "_" ^ coinductN
 val dtor_srel_coinductN = dtor_srelN ^ "_" ^ coinductN
 val strongN = "strong_"
 val dtor_map_strong_coinductN = dtor_mapN ^ "_" ^ strongN ^ coinductN
-val dtor_rel_strong_coinductN = dtor_relN ^ "_" ^ strongN ^ coinductN
+val dtor_strong_coinductN = dtorN ^ "_" ^ strongN ^ coinductN
 val dtor_srel_strong_coinductN = dtor_srelN ^ "_" ^ strongN ^ coinductN
 val hsetN = "Hset"
 val hset_recN = hsetN ^ "_rec"

--- a/src/HOL/BNF/Tools/bnf_gfp.ML	Wed Sep 26 10:00:59 2012 +0200
+++ b/src/HOL/BNF/Tools/bnf_gfp.ML	Wed Sep 26 10:00:59 2012 +0200
@@ -2180,9 +2180,8 @@
 
     val timer = time (timer "corec definitions & thms");
 
-    val (dtor_map_coinduct_thm, coinduct_params, dtor_srel_coinduct_thm, dtor_rel_coinduct_thm,
-         dtor_map_strong_coinduct_thm, dtor_srel_strong_coinduct_thm,
-         dtor_rel_strong_coinduct_thm) =
+    val (dtor_map_coinduct_thm, coinduct_params, dtor_srel_coinduct_thm, dtor_coinduct_thm,
+         dtor_map_strong_coinduct_thm, dtor_srel_strong_coinduct_thm, dtor_strong_coinduct_thm) =
       let
         val zs = Jzs1 @ Jzs2;
         val frees = phis @ zs;
@@ -2276,12 +2275,11 @@
         val rel_of_srel_thms =
           srel_defs @ @{thms Id_def' mem_Collect_eq fst_conv snd_conv split_conv};
 
-        val dtor_rel_coinduct = unfold_thms lthy rel_of_srel_thms dtor_srel_coinduct;
-        val dtor_rel_strong_coinduct = unfold_thms lthy rel_of_srel_thms dtor_srel_strong_coinduct;
+        val dtor_coinduct = unfold_thms lthy rel_of_srel_thms dtor_srel_coinduct;
+        val dtor_strong_coinduct = unfold_thms lthy rel_of_srel_thms dtor_srel_strong_coinduct;
       in
         (dtor_map_coinduct, rev (Term.add_tfrees dtor_map_coinduct_goal []), dtor_srel_coinduct,
-         dtor_rel_coinduct, dtor_map_strong_coinduct, dtor_srel_strong_coinduct,
-         dtor_rel_strong_coinduct)
+         dtor_coinduct, dtor_map_strong_coinduct, dtor_srel_strong_coinduct, dtor_strong_coinduct)
       end;
 
     val timer = time (timer "coinduction");
@@ -2963,8 +2961,8 @@
       end;
 
       val common_notes =
-        [(dtor_rel_coinductN, [dtor_rel_coinduct_thm]),
-        (dtor_rel_strong_coinductN, [dtor_rel_strong_coinduct_thm])] @
+        [(dtor_coinductN, [dtor_coinduct_thm]),
+        (dtor_strong_coinductN, [dtor_strong_coinduct_thm])] @
         (if note_all then
            [(dtor_map_coinductN, [dtor_map_coinduct_thm]),
            (dtor_map_strong_coinductN, [dtor_map_strong_coinduct_thm]),