# 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