clarified interfaces for improvable syntax

--- a/src/Pure/Isar/class.ML	Mon Jun 01 18:59:19 2015 +0200
+++ b/src/Pure/Isar/class.ML	Mon Jun 01 18:59:19 2015 +0200
@@ -294,8 +294,9 @@
   in
     ctxt
     |> fold (redeclare_const thy o fst) primary_constraints
-    |> Overloading.map_improvable_syntax (K (((primary_constraints, secondary_constraints),
-        (((improve, subst), true), unchecks)), false))
+    |> Overloading.map_improvable_syntax (K {primary_constraints = primary_constraints,
+      secondary_constraints = secondary_constraints, improve = improve, subst = subst,
+      no_subst_in_abbrev_mode = true, unchecks = unchecks})
     |> Overloading.set_primary_constraints
   end;
 
@@ -545,9 +546,10 @@
       map (fn ((c, _), v_ty as (_, ty)) => (Free v_ty, Const (c, ty))) params;
   in
     ctxt
-    |> Overloading.map_improvable_syntax
-      (fn (((primary_constraints, _), (((improve, _), _), _)), _) =>
-          (((primary_constraints, []), (((improve, subst), false), unchecks)), false))
+    |> Overloading.map_improvable_syntax (fn {primary_constraints, improve, ...} =>
+      {primary_constraints = primary_constraints, secondary_constraints = [],
+        improve = improve, subst = subst, no_subst_in_abbrev_mode = false,
+        unchecks = unchecks})
   end;
 
 fun resort_terms ctxt algebra consts constraints ts =
@@ -635,8 +637,9 @@
     |> Instantiation.put (make_instantiation ((tycos, vs, sort), params))
     |> fold (Variable.declare_typ o TFree) vs
     |> fold (Variable.declare_names o Free o snd) params
-    |> (Overloading.map_improvable_syntax o apfst)
-         (K ((primary_constraints, []), (((improve, K NONE), false), [])))
+    |> (Overloading.map_improvable_syntax) (K {primary_constraints = primary_constraints,
+      secondary_constraints = [], improve = improve, subst = K NONE,
+      no_subst_in_abbrev_mode = false, unchecks = []})
     |> Overloading.activate_improvable_syntax
     |> Context.proof_map (Syntax_Phases.term_check 0 "resorting" resort_check)
     |> synchronize_inst_syntax

--- 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) =