removed obsolete sanity check -- Sign.certify_sort is stable;
authorwenzelm
Tue Apr 27 21:53:55 2010 +0200 (2010-04-27 ago)
changeset 364300a7fdd584391
parent 36429 9d6b3be996d4
child 36445 0685b4336132
removed obsolete sanity check -- Sign.certify_sort is stable;
src/Pure/axclass.ML
     1.1 --- a/src/Pure/axclass.ML	Tue Apr 27 21:46:10 2010 +0200
     1.2 +++ b/src/Pure/axclass.ML	Tue Apr 27 21:53:55 2010 +0200
     1.3 @@ -445,7 +445,6 @@
     1.4        |> maps (these o Option.map #params o try (get_info thy))
     1.5        |> filter_out (fn (const, _) => can (get_inst_param thy) (const, t))
     1.6        |> (map o apsnd o map_atyps) (K T);
     1.7 -    val _ = map (Sign.certify_sort thy) Ss = Ss orelse err ();
     1.8      val th' = th
     1.9        |> Drule.instantiate' std_vars []
    1.10        |> Thm.unconstrain_allTs;