# HG changeset patch
# User blanchet
# Date 1393921796 -3600
# Node ID b9468e4e8c05e9828ae2389148afa5c7c25793a7
# Parent  c78575827f38793c8b9b28ea3689a64d581e627a
removed debugging leftover

diff -r c78575827f38 -r b9468e4e8c05 src/HOL/Tools/BNF/bnf_gfp.ML
--- a/src/HOL/Tools/BNF/bnf_gfp.ML	Tue Mar 04 09:07:49 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp.ML	Tue Mar 04 09:29:56 2014 +0100
@@ -2376,7 +2376,6 @@
 
       fun Jrel_coinduct_tac {context = ctxt, prems = CIHs} =
         let
-val lthy = Config.put quick_and_dirty false lthy (*XXX*)
           fun mk_helper_prem phi in_phi zip x y map map' dtor dtor' =
             let
               val zipxy = zip $ x $ y;