author | immler |
Wed, 13 Jun 2018 09:38:07 +0200 | |
changeset 68436 | 1b3edf5da4e4 |
parent 68435 | 2a2ef4552aaf |
child 68437 | f9b15e7c12bd |
--- 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