src/HOL/Nat.thy
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