# HG changeset patch
# User desharna
# Date 1405585749 -7200
# Node ID 2c65870c706fbfe9abd19a7b3fc6a445b1f12cd9
# Parent  d554b0097ad4d7d1fbf651fd5787cf5a5a6496fe
fix bug caused by bad context

diff -r d554b0097ad4 -r 2c65870c706f src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Thu Jul 17 10:28:32 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Thu Jul 17 10:29:09 2014 +0200
@@ -1556,7 +1556,7 @@
                           fun travese_nested_types t ctxt =
                             (case fastype_of t of
                               Type (type_name, xs) =>
-                              (case bnf_of lthy type_name of
+                              (case bnf_of ctxt type_name of
                                 NONE => ([], ctxt)
                               | SOME bnf =>
                                 let
@@ -1583,7 +1583,7 @@
                             if sel_rangeT = A then
                               ([mk_Trueprop_mem (selA $ ta, setA $ ta)], ctxt)
                             else
-                              travese_nested_types (selA $ ta) names_lthy;
+                              travese_nested_types (selA $ ta) ctxt;
                         in
                           if exists_subtype_in [A] sel_rangeT then
                             if is_refl_bool prem then