src/HOL/Types_To_Sets/unoverload_type.ML

--- a/src/HOL/Types_To_Sets/unoverload_type.ML	Wed Jun 13 09:26:04 2018 +0200
+++ b/src/HOL/Types_To_Sets/unoverload_type.ML	Wed Jun 13 09:38:07 2018 +0200
@@ -53,6 +53,7 @@
         map (apsnd (map_type_tfree (fn ("'a", _) =>  tvar | x => TFree x)))
     in
       fold (fn c => Unoverloading.unoverload (Thm.global_cterm_of thy (Const c))) consts thm'
+      |> Raw_Simplifier.norm_hhf (Context.proof_of context)
     end
   end