fix bug caused by bad context
authordesharna
Thu Jul 17 10:29:09 2014 +0200 (2014-07-17)
changeset 575682c65870c706f
parent 57567 d554b0097ad4
child 57569 e20a999f7161
fix bug caused by bad context
src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
     1.1 --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Thu Jul 17 10:28:32 2014 +0200
     1.2 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Thu Jul 17 10:29:09 2014 +0200
     1.3 @@ -1556,7 +1556,7 @@
     1.4                            fun travese_nested_types t ctxt =
     1.5                              (case fastype_of t of
     1.6                                Type (type_name, xs) =>
     1.7 -                              (case bnf_of lthy type_name of
     1.8 +                              (case bnf_of ctxt type_name of
     1.9                                  NONE => ([], ctxt)
    1.10                                | SOME bnf =>
    1.11                                  let
    1.12 @@ -1583,7 +1583,7 @@
    1.13                              if sel_rangeT = A then
    1.14                                ([mk_Trueprop_mem (selA $ ta, setA $ ta)], ctxt)
    1.15                              else
    1.16 -                              travese_nested_types (selA $ ta) names_lthy;
    1.17 +                              travese_nested_types (selA $ ta) ctxt;
    1.18                          in
    1.19                            if exists_subtype_in [A] sel_rangeT then
    1.20                              if is_refl_bool prem then