src/HOL/Tools/inductive_codegen.ML

 fun print_modes modes = message ("Inferred modes:\n" ^
   space_implode "\n" (map (fn (s, ms) => s ^ ": " ^ commas (map
     string_of_mode ms)) modes));
 
 val term_vs = map (fst o fst o dest_Var) o term_vars;
-val terms_vs = distinct o List.concat o (map term_vs);
+val terms_vs = distinct (op =) o List.concat o (map term_vs);
 
 (** collect all Vars in a term (with duplicates!) **)
 fun term_vTs tm =
   fold_aterms (fn Var ((x, _), T) => cons (x, T) | _ => I) tm [];
 

               (Pretty.block [Pretty.str "Seq.single", Pretty.brk 1, mk_tuple out_ps])
               (exists (not o is_exhaustive) out_ts'''))
           end
       | compile_prems out_ts vs names gr ps =
           let
-            val vs' = distinct (List.concat (vs :: map term_vs out_ts));
+            val vs' = distinct (op =) (List.concat (vs :: map term_vs out_ts));
             val SOME (p, mode as SOME (Mode ((_, js), _))) =
               select_mode_prem thy modes' vs' ps;
             val ps' = filter_out (equal p) ps;
             val ((names', eqs), out_ts') =
               foldl_map check_constrt ((names, []), out_ts);