src/Pure/axclass.ML
changeset 22691 290454649b8c
parent 22570 f166a5416b3f
child 22745 17bc6af2011e
     1.1 --- a/src/Pure/axclass.ML	Sun Apr 15 14:31:44 2007 +0200
     1.2 +++ b/src/Pure/axclass.ML	Sun Apr 15 14:31:47 2007 +0200
     1.3 @@ -214,7 +214,7 @@
     1.4  fun add_classrel th thy =
     1.5    let
     1.6      fun err () = raise THM ("add_classrel: malformed class relation", 0, [th]);
     1.7 -    val prop = Drule.plain_prop_of (Thm.transfer thy th);
     1.8 +    val prop = Thm.plain_prop_of (Thm.transfer thy th);
     1.9      val rel = Logic.dest_classrel prop handle TERM _ => err ();
    1.10      val (c1, c2) = cert_classrel thy rel handle TYPE _ => err ();
    1.11    in
    1.12 @@ -226,7 +226,7 @@
    1.13  fun add_arity th thy =
    1.14    let
    1.15      fun err () = raise THM ("add_arity: malformed type arity", 0, [th]);
    1.16 -    val prop = Drule.plain_prop_of (Thm.transfer thy th);
    1.17 +    val prop = Thm.plain_prop_of (Thm.transfer thy th);
    1.18      val (t, Ss, c) = Logic.dest_arity prop handle TERM _ => err ();
    1.19      val _ = if map (Sign.certify_sort thy) Ss = Ss then () else err ();
    1.20    in