# HG changeset patch
# User wenzelm
# Date 1273930293 -7200
# Node ID a3715d7ff337a7c498d65ef1490dcfe3626084cf
# Parent  ae0809cff6f05889037d96af57194f23e2a18ef4
eliminated redundant runtime checks;

diff -r ae0809cff6f0 -r a3715d7ff337 src/Pure/axclass.ML
--- a/src/Pure/axclass.ML	Sat May 15 00:45:42 2010 +0200
+++ b/src/Pure/axclass.ML	Sat May 15 15:31:33 2010 +0200
@@ -412,8 +412,6 @@
 
 (* primitive rules *)
 
-val shyps_topped = forall null o #shyps o Thm.rep_thm;
-
 fun add_classrel raw_th thy =
   let
     val th = Thm.strip_shyps (Thm.transfer thy raw_th);
@@ -424,7 +422,6 @@
     val th' = th
       |> Thm.unconstrainT
       |> Drule.instantiate' [SOME (ctyp_of thy (TVar ((Name.aT, 0), [])))] [];
-    val _ = shyps_topped th' orelse raise Fail "add_classrel: nontop shyps after unconstrain";
   in
     thy
     |> Sign.primitive_classrel (c1, c2)
@@ -450,7 +447,6 @@
     val th' = th
       |> Thm.unconstrainT
       |> Drule.instantiate' std_vars [];
-    val _ = shyps_topped th' orelse raise Fail "add_arity: nontop shyps after unconstrain";
   in
     thy
     |> fold (#2 oo declare_overloaded) missing_params