tuned;

--- a/src/HOL/Tools/code_evaluation.ML	Sun Apr 10 23:15:34 2016 +0200
+++ b/src/HOL/Tools/code_evaluation.ML	Mon Apr 11 11:48:24 2016 +0200
@@ -165,9 +165,9 @@
       | NONE => NONE)
   | subst_termify t = subst_termify_app (strip_comb t) 
 
-fun check_termify _ ts = the_default ts (map_default subst_termify ts);
+fun check_termify ts = the_default ts (map_default subst_termify ts);
 
-val _ = Context.>> (Syntax_Phases.term_check 0 "termify" check_termify);
+val _ = Context.>> (Syntax_Phases.term_check 0 "termify" (K check_termify));
 
 
 (** evaluation **)

--- a/src/Pure/Isar/class_declaration.ML	Sun Apr 10 23:15:34 2016 +0200
+++ b/src/Pure/Isar/class_declaration.ML	Mon Apr 11 11:48:24 2016 +0200
@@ -107,7 +107,6 @@
 
 fun prep_class_elems prep_decl thy sups raw_elems =
   let
-
     (* user space type system: only permits 'a type variable, improves towards 'a *)
     val algebra = Sign.classes_of thy;
     val inter_sort = curry (Sorts.inter_sort algebra);
@@ -118,7 +117,7 @@
     val base_constraints = (map o apsnd)
       (map_type_tfree (K (TVar ((Name.aT, 0), proto_base_sort))) o fst o fst o snd)
         (Class.these_operations thy sups);
-    fun singleton_fixateT Ts =
+    val singleton_fixate = burrow_types (fn Ts =>
       let
         val tfrees = fold Term.add_tfreesT Ts [];
         val inferred_sort =
@@ -140,9 +139,8 @@
       in
         (map o map_atyps)
           (fn T as TVar (xi, _) => if Type_Infer.is_param xi then fixateT else T | T => T) Ts
-      end;
-    fun singleton_fixate _ ts = burrow_types singleton_fixateT ts;
-    fun unify_params ctxt ts =
+      end);
+    fun unify_params ts =
       let
         val param_Ts = (fold o fold_aterms)
           (fn Free (v, T) => if is_param v then fold_atyps (insert (op =)) T else I | _ => I) ts [];
@@ -162,10 +160,10 @@
     val init_class_body =
       fold (Proof_Context.add_const_constraint o apsnd SOME) base_constraints
       #> Class.redeclare_operations thy sups
-      #> Context.proof_map (Syntax_Phases.term_check 0 "singleton_fixate" singleton_fixate);
+      #> Context.proof_map (Syntax_Phases.term_check 0 "singleton_fixate" (K singleton_fixate));
     val ((raw_supparams, _, raw_inferred_elems, _), _) =
       Proof_Context.init_global thy
-      |> Context.proof_map (Syntax_Phases.term_check 0 "unify_params" unify_params)
+      |> Context.proof_map (Syntax_Phases.term_check 0 "unify_params" (K unify_params))
       |> prep_decl raw_supexpr init_class_body raw_elems;
     fun filter_element (Element.Fixes []) = NONE
       | filter_element (e as Element.Fixes _) = SOME e

--- a/src/Pure/Syntax/syntax_phases.ML	Sun Apr 10 23:15:34 2016 +0200
+++ b/src/Pure/Syntax/syntax_phases.ML	Mon Apr 11 11:48:24 2016 +0200
@@ -970,18 +970,7 @@
 end;
 
 
-(* standard phases *)
-
-val _ = Context.>>
- (typ_check 0 "standard" Proof_Context.standard_typ_check #>
-  term_check 0 "standard"
-    (fn ctxt => Type_Infer_Context.infer_types ctxt #> map (Proof_Context.expand_abbrevs ctxt)) #>
-  term_check 100 "standard_finish" Proof_Context.standard_term_check_finish #>
-  term_uncheck 0 "standard" Proof_Context.standard_term_uncheck);
-
-
-
-(** install operations **)
+(* install operations *)
 
 val _ =
   Theory.setup
@@ -1000,3 +989,13 @@
       uncheck_terms = uncheck_terms});
 
 end;
+
+
+(* standard phases *)
+
+val _ = Context.>>
+ (Syntax_Phases.typ_check 0 "standard" Proof_Context.standard_typ_check #>
+  Syntax_Phases.term_check 0 "standard"
+    (fn ctxt => Type_Infer_Context.infer_types ctxt #> map (Proof_Context.expand_abbrevs ctxt)) #>
+  Syntax_Phases.term_check 100 "standard_finish" Proof_Context.standard_term_check_finish #>
+  Syntax_Phases.term_uncheck 0 "standard" Proof_Context.standard_term_uncheck);