--- 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