diff -r c7ca6bb006b0 -r a808b57d5b0d src/Pure/Isar/overloading.ML
--- a/src/Pure/Isar/overloading.ML	Mon Jun 01 18:59:19 2015 +0200
+++ b/src/Pure/Isar/overloading.ML	Mon Jun 01 18:59:19 2015 +0200
@@ -21,63 +21,46 @@
 
 (* generic check/uncheck combinators for improvable constants *)
 
-type improvable_syntax = ((((string * typ) list * (string * typ) list) *
-  ((((string * typ -> (typ * typ) option) * (string * typ -> (typ * term) option)) * bool) *
-    (term * term) list)) * bool);
+type improvable_syntax = {
+  primary_constraints: (string * typ) list,
+  secondary_constraints: (string * typ) list,
+  improve: string * typ -> (typ * typ) option,
+  subst: string * typ -> (typ * term) option,
+  no_subst_in_abbrev_mode: bool,
+  unchecks: (term * term) list
+}
 
 structure Improvable_Syntax = Proof_Data
 (
-  type T = {
-    primary_constraints: (string * typ) list,
-    secondary_constraints: (string * typ) list,
-    improve: string * typ -> (typ * typ) option,
-    subst: string * typ -> (typ * term) option,
-    consider_abbrevs: bool,
-    unchecks: (term * term) list,
-    passed: bool
-  };
-  val empty: T = {
-    primary_constraints = [],
-    secondary_constraints = [],
-    improve = K NONE,
-    subst = K NONE,
-    consider_abbrevs = false,
-    unchecks = [],
-    passed = true
-  };
-  fun init _ = empty;
+  type T = {syntax: improvable_syntax, secondary_pass: bool}
+  fun init _ = {syntax = {
+      primary_constraints = [],
+      secondary_constraints = [],
+      improve = K NONE,
+      subst = K NONE,
+      no_subst_in_abbrev_mode = false,
+      unchecks = []
+    }, secondary_pass = false}: T;
 );
 
-fun map_improvable_syntax f = Improvable_Syntax.map (fn {primary_constraints,
-    secondary_constraints, improve, subst, consider_abbrevs, unchecks, passed} =>
-  let
-    val (((primary_constraints', secondary_constraints'),
-      (((improve', subst'), consider_abbrevs'), unchecks')), passed')
-        = f (((primary_constraints, secondary_constraints),
-            (((improve, subst), consider_abbrevs), unchecks)), passed)
-  in
-   {primary_constraints = primary_constraints', secondary_constraints = secondary_constraints',
-    improve = improve', subst = subst', consider_abbrevs = consider_abbrevs',
-    unchecks = unchecks', passed = passed'}
-  end);
+fun map_improvable_syntax f =
+  Improvable_Syntax.map (fn {syntax, secondary_pass} => {syntax = f syntax, secondary_pass = secondary_pass});
 
-val mark_passed = (map_improvable_syntax o apsnd) (K true);
+val mark_passed =
+  Improvable_Syntax.map (fn {syntax, secondary_pass} => {syntax = syntax, secondary_pass = true});
 
 fun improve_term_check ts ctxt =
   let
     val thy = Proof_Context.theory_of ctxt;
 
-    val {secondary_constraints, improve, subst, consider_abbrevs, passed, ...} =
+    val {syntax = {secondary_constraints, improve, subst, no_subst_in_abbrev_mode, ...}, secondary_pass} =
       Improvable_Syntax.get ctxt;
-    val is_abbrev = consider_abbrevs andalso Proof_Context.abbrev_mode ctxt;
-    val passed_or_abbrev = passed orelse is_abbrev;
+    val no_subst = Proof_Context.abbrev_mode ctxt andalso no_subst_in_abbrev_mode;
     fun accumulate_improvements (Const (c, ty)) =
           (case improve (c, ty) of
             SOME ty_ty' => Sign.typ_match thy ty_ty'
           | _ => I)
       | accumulate_improvements _ = I;
-    val improvements = (fold o fold_aterms) accumulate_improvements ts Vartab.empty;
-    val ts' = (map o map_types) (Envir.subst_type improvements) ts;
     fun apply_subst t =
       Envir.expand_term
         (fn Const (c, ty) =>
@@ -87,12 +70,17 @@
               then SOME (ty', apply_subst t') else NONE
           | NONE => NONE)
         | _ => NONE) t;
-    val ts'' = if is_abbrev then ts' else map apply_subst ts';
+    val improvements = (fold o fold_aterms) accumulate_improvements ts Vartab.empty;
+    val ts' =
+      ts
+      |> (map o map_types) (Envir.subst_type improvements)
+      |> not no_subst ? map apply_subst;
   in
-    if eq_list (op aconv) (ts, ts'') andalso passed_or_abbrev then NONE
-    else if passed_or_abbrev then SOME (ts'', ctxt)
+    if secondary_pass orelse no_subst then
+      if eq_list (op aconv) (ts, ts') then NONE
+      else SOME (ts', ctxt)
     else
-      SOME (ts'', ctxt
+      SOME (ts', ctxt
         |> fold (Proof_Context.add_const_constraint o apsnd SOME) secondary_constraints
         |> mark_passed)
   end;
@@ -105,12 +93,13 @@
 fun improve_term_uncheck ts ctxt =
   let
     val thy = Proof_Context.theory_of ctxt;
-    val {unchecks, ...} = Improvable_Syntax.get ctxt;
+    val {syntax = {unchecks, ...}, ...} = Improvable_Syntax.get ctxt;
     val ts' = map (rewrite_liberal thy unchecks) ts;
   in if exists is_some ts' then SOME (map2 the_default ts ts', ctxt) else NONE end;
 
 fun set_primary_constraints ctxt =
-  let val {primary_constraints, ...} = Improvable_Syntax.get ctxt;
+  let
+    val {syntax = {primary_constraints, ...}, ...} = Improvable_Syntax.get ctxt;
   in fold (Proof_Context.add_const_constraint o apsnd SOME) primary_constraints ctxt end;
 
 val activate_improvable_syntax =
@@ -147,7 +136,9 @@
       map (fn (c_ty as (_, ty), (v, _)) => (Free (v, ty), Const c_ty)) overloading;
   in 
     ctxt
-    |> map_improvable_syntax (K ((([], []), (((K NONE, subst), false), unchecks)), false))
+    |> map_improvable_syntax (K {primary_constraints = [],
+      secondary_constraints = [], improve = K NONE, subst = subst,
+      no_subst_in_abbrev_mode = false, unchecks = unchecks})
   end;
 
 fun define_overloaded (c, U) (v, checked) (b_def, rhs) =