# HG changeset patch
# User wenzelm
# Date 1441040664 -7200
# Node ID ca4ebc63d8aca4cb1d70b3495b8594c65894d663
# Parent  01b23bfb49478fd0bb57ab7bdf5555e10ec8e6e7
clarified context;

diff -r 01b23bfb4947 -r ca4ebc63d8ac src/HOL/Tools/Ctr_Sugar/ctr_sugar_code.ML
--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar_code.ML	Mon Aug 31 19:04:01 2015 +0200
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar_code.ML	Mon Aug 31 19:04:24 2015 +0200
@@ -93,7 +93,7 @@
           |> Syntax.check_term lthy;
         val ((_, (_, raw_def)), lthy') =
           Specification.definition (NONE, (Attrib.empty_binding, spec)) lthy;
-        val thy_ctxt = Proof_Context.init_global (Proof_Context.theory_of lthy); (* FIXME? *)
+        val thy_ctxt = Proof_Context.init_global (Proof_Context.theory_of lthy');
         val def = singleton (Proof_Context.export lthy' thy_ctxt) raw_def;
       in
         (def, lthy')