--- 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