changeset 62958 | b41c1cb5e251 |
parent 62334 | 15176172701e |
child 64434 | af5235830c16 |
--- a/src/HOL/Tools/Transfer/transfer.ML Tue Apr 12 13:49:37 2016 +0200 +++ b/src/HOL/Tools/Transfer/transfer.ML Tue Apr 12 14:38:57 2016 +0200 @@ -518,8 +518,7 @@ end | go _ ctxt = dummy ctxt in - go t ctxt |> fst |> Syntax.check_term ctxt |> - map_types (map_type_tfree (fn (a, _) => TFree (a, @{sort type}))) + go t ctxt |> fst |> Syntax.check_term ctxt end (** Monotonicity analysis **)