author | wenzelm |
Tue, 27 Apr 2010 21:53:55 +0200 | |
changeset 36430 | 0a7fdd584391 |
parent 36429 | 9d6b3be996d4 |
child 36445 | 0685b4336132 |
--- 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;