--- a/src/HOL/Nat.thy Thu Jul 20 14:05:29 2017 +0100
+++ b/src/HOL/Nat.thy Thu Jul 20 16:28:43 2017 +0100
@@ -163,8 +163,8 @@
BNF_LFP_Rec_Sugar.default_basic_lfp_sugars_of bs arg_Ts callers callssss ctxt;
in
BNF_LFP_Rec_Sugar.register_lfp_rec_extension
- {nested_simps = [], is_new_datatype = K (K true), basic_lfp_sugars_of = basic_lfp_sugars_of,
- rewrite_nested_rec_call = NONE}
+ {nested_simps = [], special_endgame_tac = K (K (K (K no_tac))), is_new_datatype = K (K true),
+ basic_lfp_sugars_of = basic_lfp_sugars_of, rewrite_nested_rec_call = NONE}
end
\<close>