src/Pure/axclass.ML
changeset 36935 a3715d7ff337
parent 36934 ae0809cff6f0
child 37232 c10fb22a5e0c
     1.1 --- a/src/Pure/axclass.ML	Sat May 15 00:45:42 2010 +0200
     1.2 +++ b/src/Pure/axclass.ML	Sat May 15 15:31:33 2010 +0200
     1.3 @@ -412,8 +412,6 @@
     1.4  
     1.5  (* primitive rules *)
     1.6  
     1.7 -val shyps_topped = forall null o #shyps o Thm.rep_thm;
     1.8 -
     1.9  fun add_classrel raw_th thy =
    1.10    let
    1.11      val th = Thm.strip_shyps (Thm.transfer thy raw_th);
    1.12 @@ -424,7 +422,6 @@
    1.13      val th' = th
    1.14        |> Thm.unconstrainT
    1.15        |> Drule.instantiate' [SOME (ctyp_of thy (TVar ((Name.aT, 0), [])))] [];
    1.16 -    val _ = shyps_topped th' orelse raise Fail "add_classrel: nontop shyps after unconstrain";
    1.17    in
    1.18      thy
    1.19      |> Sign.primitive_classrel (c1, c2)
    1.20 @@ -450,7 +447,6 @@
    1.21      val th' = th
    1.22        |> Thm.unconstrainT
    1.23        |> Drule.instantiate' std_vars [];
    1.24 -    val _ = shyps_topped th' orelse raise Fail "add_arity: nontop shyps after unconstrain";
    1.25    in
    1.26      thy
    1.27      |> fold (#2 oo declare_overloaded) missing_params