src/HOL/Tools/BNF/bnf_fp_def_sugar.ML

--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Wed Oct 05 21:27:21 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Thu Oct 06 13:33:26 2016 +0200
@@ -847,7 +847,7 @@
           in
             Goal.prove_sorry lthy vars [] goal (fn {context = ctxt, prems = _} =>
               mk_map_tac ctxt abs_inverses pre_map_def dtor_ctor fp_map_thm'
-                live_nesting_map_ident0s ctr_defs' extra_unfolds_map)
+                live_nesting_map_id0s ctr_defs' extra_unfolds_map)
             |> Thm.close_derivation
             |> Conjunction.elim_balanced (length goals)
           end;