src/HOL/Types_To_Sets/unoverload_type.ML
changeset 68436 1b3edf5da4e4
parent 68435 2a2ef4552aaf
child 68437 f9b15e7c12bd
     1.1 --- a/src/HOL/Types_To_Sets/unoverload_type.ML	Wed Jun 13 09:26:04 2018 +0200
     1.2 +++ b/src/HOL/Types_To_Sets/unoverload_type.ML	Wed Jun 13 09:38:07 2018 +0200
     1.3 @@ -53,6 +53,7 @@
     1.4          map (apsnd (map_type_tfree (fn ("'a", _) =>  tvar | x => TFree x)))
     1.5      in
     1.6        fold (fn c => Unoverloading.unoverload (Thm.global_cterm_of thy (Const c))) consts thm'
     1.7 +      |> Raw_Simplifier.norm_hhf (Context.proof_of context)
     1.8      end
     1.9    end
    1.10