# HG changeset patch
# User blanchet
# Date 1410428987 -7200
# Node ID 759e47518d80a3e0f7ae3a6b98104768977937b6
# Parent  c8a8e7c37986eeb925c516a3dfbe9594c6799c96
comment

diff -r c8a8e7c37986 -r 759e47518d80 src/HOL/Library/bnf_lfp_countable.ML
--- a/src/HOL/Library/bnf_lfp_countable.ML	Wed Sep 10 22:52:46 2014 +0200
+++ b/src/HOL/Library/bnf_lfp_countable.ML	Thu Sep 11 11:49:47 2014 +0200
@@ -169,7 +169,7 @@
       val conjuncts = map3 mk_conjunct fpTs xs (mk_encode_funs ctxt fpTs ns ctrss0 recs0);
       val goal = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj conjuncts);
     in
-      Goal.prove ctxt [] [] goal (fn {context = ctxt, prems = _} =>
+      Goal.prove (*no sorry*) ctxt [] [] goal (fn {context = ctxt, prems = _} =>
         mk_encode_injectives_tac ctxt ns induct nchotomys injectss rec_thmss map_comps'
           inj_map_strongs')
       |> HOLogic.conj_elims