--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar_code.ML Fri Mar 06 23:57:01 2015 +0100
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar_code.ML Sat Mar 07 00:45:15 2015 +0100
@@ -87,8 +87,8 @@
|> Syntax.check_term lthy;
val ((_, (_, raw_def)), lthy') =
Specification.definition (NONE, (Attrib.empty_binding, spec)) lthy;
- val ctxt_thy = Proof_Context.init_global (Proof_Context.theory_of lthy); (* FIXME? *)
- val def = singleton (Proof_Context.export lthy' ctxt_thy) raw_def;
+ val thy_ctxt = Proof_Context.init_global (Proof_Context.theory_of lthy); (* FIXME? *)
+ val def = singleton (Proof_Context.export lthy' thy_ctxt) raw_def;
in
(def, lthy')
end;