--- a/src/Pure/Isar/overloading.ML Mon Apr 26 16:08:04 2010 +0200
+++ b/src/Pure/Isar/overloading.ML Mon Apr 26 20:30:50 2010 +0200
@@ -67,8 +67,8 @@
fun improve_term_check ts ctxt =
let
- val { primary_constraints, secondary_constraints, improve, subst,
- consider_abbrevs, passed, ... } = ImprovableSyntax.get ctxt;
+ val { secondary_constraints, improve, subst, consider_abbrevs, passed, ... } =
+ ImprovableSyntax.get ctxt;
val tsig = (Sign.tsig_of o ProofContext.theory_of) ctxt;
val is_abbrev = consider_abbrevs andalso ProofContext.abbrev_mode ctxt;
val passed_or_abbrev = passed orelse is_abbrev;