Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
clarified context;
authorwenzelm
Mon, 31 Aug 2015 19:04:24 +0200
changeset 61065 ca4ebc63d8ac
parent 61064 01b23bfb4947
child 61066 00a169fe5de4
clarified context;
src/HOL/Tools/Ctr_Sugar/ctr_sugar_code.ML file | annotate | diff | comparison | revisions 
--- 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')
isabelle