src/Pure/Isar/class.ML

 
   val class: bstring -> class list -> Element.context_i Locale.element list
     -> string list -> theory -> string * Proof.context
   val class_cmd: bstring -> xstring list -> Element.context Locale.element list
     -> xstring list -> theory -> string * Proof.context
-  val init: class -> Proof.context -> Proof.context;
+  val init: class -> Proof.context -> Proof.context
   val add_const_in_class: string -> (string * mixfix) * (string * term)
     -> theory -> string * theory
   val add_abbrev_in_class: string -> Syntax.mode -> (string * mixfix) * (string * term)
     -> theory -> string * theory
   val remove_constraint: class -> string -> Proof.context -> Proof.context

     val ts' = map (map_aterms
         (fn t as Const (c, ty) => the_default t (AList.lookup (op =) cs (c, ty)) | t => t)
       #> (map_types o map_type_tvar) (fn var as (vi, _) => if member (op =) typarams vi
            then TFree (Name.aT, local_sort) else TVar var)) ts;
     val ctxt' = fold (ProofContext.add_const_constraint o apsnd SOME) constraints ctxt;
-  in (ts', ctxt') end;
+  in if eq_list (op aconv) (ts, ts') then NONE else SOME (ts', ctxt') end;
 
 val uncheck = ref false;
 
 fun sort_term_uncheck sups ts ctxt =
   let

       | globalize (t as Const (c, ty)) = (case global_operation c
          of SOME c => Const (c, ty)
           | NONE => t)
       | globalize t = t;
     val ts' = if ! uncheck then (map o map_aterms) globalize ts else ts;
-  in (ts', ctxt) end;
+  in if eq_list (op aconv) (ts, ts') then NONE else SOME (ts', ctxt) end;
 
 fun init_class_ctxt sups local_sort ctxt =
   let
     val operations = these_operations (ProofContext.theory_of ctxt) sups;
   in