src/Pure/axclass.ML
changeset 36768 46be86127972
parent 36740 6248aa22c694
child 36881 4de023c28a84
     1.1 --- a/src/Pure/axclass.ML	Sun May 09 18:09:30 2010 +0200
     1.2 +++ b/src/Pure/axclass.ML	Sun May 09 19:15:21 2010 +0200
     1.3 @@ -423,7 +423,7 @@
     1.4      val (c1, c2) = cert_classrel thy rel handle TYPE _ => err ();
     1.5      val th' = th
     1.6        |> Drule.instantiate' [SOME (ctyp_of thy (TVar ((Name.aT, 0), [c1])))] []
     1.7 -      |> Thm.unconstrain_allTs;
     1.8 +      |> Thm.unconstrainT;
     1.9      val _ = shyps_topped th' orelse raise Fail "add_classrel: nontop shyps after unconstrain";
    1.10    in
    1.11      thy
    1.12 @@ -449,7 +449,7 @@
    1.13        |> (map o apsnd o map_atyps) (K T);
    1.14      val th' = th
    1.15        |> Drule.instantiate' std_vars []
    1.16 -      |> Thm.unconstrain_allTs;
    1.17 +      |> Thm.unconstrainT;
    1.18      val _ = shyps_topped th' orelse raise Fail "add_arity: nontop shyps after unconstrain";
    1.19    in
    1.20      thy