src/HOL/Tools/BNF/bnf_comp.ML

--- a/src/HOL/Tools/BNF/bnf_comp.ML	Sun Aug 10 20:45:48 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_comp.ML	Mon Aug 11 10:43:03 2014 +0200
@@ -203,7 +203,7 @@
         fun tac {context = ctxt, prems = _} =
           mk_simplified_set_tac ctxt (collect_set_map_of_bnf outer);
         val set'_eq_set =
-          Goal.prove names_lthy [] [] goal tac
+          Goal.prove (*no sorry*) names_lthy [] [] goal tac
           |> Thm.close_derivation;
         val set' = fst (HOLogic.dest_eq (HOLogic.dest_Trueprop (Thm.prop_of set'_eq_set)));
       in