Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/BNF/bnf_fp_n2m.ML
changeset 60728 26ffdb966759
parent 59860 a979fc5db526
child 60788 5e2df6bd906c 
--- a/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Thu Jul 16 10:48:20 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Thu Jul 16 12:23:22 2015 +0200
@@ -462,7 +462,7 @@
           unfold_thms_tac ctxt (flat [rec_thms, raw_co_rec_defs, pre_map_defs,
             fp_pre_map_defs, fp_xtor_co_recs, fp_rec_o_maps, map_thms, fp_Rep_o_Abss,
             Rep_o_Abss]) THEN
-          CONJ_WRAP (K (HEADGOAL (rtac refl))) bnfs;
+          CONJ_WRAP (K (HEADGOAL (rtac ctxt refl))) bnfs;
       in
         Library.foldr1 HOLogic.mk_conj goals
         |> HOLogic.mk_Trueprop
isabelle