use right local theory -- shows up when 'no_discs_sels' is set
authorblanchet
Wed, 12 Feb 2014 08:35:56 +0100
changeset 55407 81f7e60755c3
parent 55406 186076d100d3
child 55408 479a779b89a6
use right local theory -- shows up when 'no_discs_sels' is set
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);