changeset 62326 | 3cf7a067599c |
parent 62217 | 527488dc8b90 |
child 62344 | 759d684c0e60 |
--- a/src/HOL/Nat.thy Tue Feb 16 22:28:19 2016 +0100 +++ b/src/HOL/Nat.thy Wed Feb 17 11:54:34 2016 +0100 @@ -167,7 +167,7 @@ setup \<open> let fun basic_lfp_sugars_of _ [@{typ nat}] _ _ ctxt = - ([], [0], [nat_basic_lfp_sugar], [], [], TrueI (*dummy*), [], false, ctxt) + ([], [0], [nat_basic_lfp_sugar], [], [], [], TrueI (*dummy*), [], false, ctxt) | basic_lfp_sugars_of bs arg_Ts callers callssss ctxt = BNF_LFP_Rec_Sugar.default_basic_lfp_sugars_of bs arg_Ts callers callssss ctxt; in