changeset 36430 | 0a7fdd584391 |
parent 36427 | 85bc9b7c4d18 |
child 36456 | 9fd0f1eacd35 |
--- a/src/Pure/axclass.ML Tue Apr 27 21:46:10 2010 +0200 +++ b/src/Pure/axclass.ML Tue Apr 27 21:53:55 2010 +0200 @@ -445,7 +445,6 @@ |> maps (these o Option.map #params o try (get_info thy)) |> filter_out (fn (const, _) => can (get_inst_param thy) (const, t)) |> (map o apsnd o map_atyps) (K T); - val _ = map (Sign.certify_sort thy) Ss = Ss orelse err (); val th' = th |> Drule.instantiate' std_vars [] |> Thm.unconstrain_allTs;