src/Pure/axclass.ML
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;