# HG changeset patch
# User wenzelm
# Date 1272398035 -7200
# Node ID 0a7fdd584391b4c842e6e25870aaa80bd50132aa
# Parent  9d6b3be996d4f405a2ab1d26ad7fe45c86ad9e92
removed obsolete sanity check -- Sign.certify_sort is stable;

diff -r 9d6b3be996d4 -r 0a7fdd584391 src/Pure/axclass.ML
--- 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;