# HG changeset patch
# User blanchet
# Date 1392190556 -3600
# Node ID 81f7e60755c331f4ef15416e6275a2c0dcdf2ffd
# Parent  186076d100d305c062ef97687fc4165193f5373e
use right local theory -- shows up when 'no_discs_sels' is set

diff -r 186076d100d3 -r 81f7e60755c3 src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML
--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Wed Feb 12 08:35:56 2014 +0100
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Wed Feb 12 08:35:56 2014 +0100
@@ -439,7 +439,7 @@
 
     val (all_sels_distinct, discs, selss, disc_defs, sel_defs, sel_defss, lthy') =
       if no_discs_sels then
-        (true, [], [], [], [], [], lthy)
+        (true, [], [], [], [], [], lthy')
       else
         let
           fun disc_free b = Free (Binding.name_of b, mk_pred1T fcT);