# HG changeset patch
# User immler
# Date 1528875487 -7200
# Node ID 1b3edf5da4e4275157f4db4507fe5497969b013f
# Parent  2a2ef4552aafe8b9d41c1b81a88bf34b0837c19c
result of unoverload is not in normal form

diff -r 2a2ef4552aaf -r 1b3edf5da4e4 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