# HG changeset patch
# User blanchet
# Date 1459241822 -7200
# Node ID 1ddfe28117e90313efc235f88037800eaf9715c7
# Parent  69e4a4fffea99f6ff88a80a49d489e87d13dfdff
renamed generated theorem

diff -r 69e4a4fffea9 -r 1ddfe28117e9 src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML	Tue Mar 29 09:49:39 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML	Tue Mar 29 10:57:02 2016 +0200
@@ -54,7 +54,6 @@
 val symN = "sym";
 val transN = "trans";
 val cong_introsN = prefix cong_N "intros";
-val cong_intros_friendN = "cong_intros_friend";
 val codeN = "code";
 val coinductN = "coinduct";
 val coinduct_uptoN = "coinduct_upto";
@@ -2303,9 +2302,9 @@
         val unique = derive_unique lthy Morphism.identity code_goal corec_info res_T eq_corecUU;
 
         val notes =
-          [(cong_intros_friendN, maps snd cong_intros_pairs, []),
-           (codeN, [code_thm], []),
+          [(codeN, [code_thm], []),
            (coinductN, [coinduct], coinduct_attrs),
+           (cong_introsN, maps snd cong_intros_pairs, []),
            (uniqueN, [unique], [])] @
            map (fn (thmN, thms) => (thmN, thms, [])) cong_intros_pairs @
           (if Config.get lthy bnf_internals then