--- a/src/HOL/Tools/BNF/bnf_lfp_size.ML Fri Mar 06 23:57:01 2015 +0100
+++ b/src/HOL/Tools/BNF/bnf_lfp_size.ML Sat Mar 07 00:45:15 2015 +0100
@@ -212,8 +212,8 @@
val (thm, lthy') = lthy
|> Local_Theory.define ((Binding.name c, NoSyn), ((def_b, []), rhs))
|-> (fn (t, (_, thm)) => Spec_Rules.add Spec_Rules.Equational ([t], [thm]) #> pair thm);
- val ctxt_thy = Proof_Context.init_global (Proof_Context.theory_of lthy');
- val thm' = singleton (Proof_Context.export lthy' ctxt_thy) thm;
+ val thy_ctxt = Proof_Context.init_global (Proof_Context.theory_of lthy');
+ val thm' = singleton (Proof_Context.export lthy' thy_ctxt) thm;
in (thm', lthy') end;
val (overloaded_size_defs, lthy2) = lthy1