src/Pure/axclass.ML
changeset 31948 ea8c8bf47ce3
parent 31944 c8a35979a5bc
child 32197 bc341bbe4417
     1.1 --- a/src/Pure/axclass.ML	Mon Jul 06 22:42:27 2009 +0200
     1.2 +++ b/src/Pure/axclass.ML	Tue Jul 07 00:29:34 2009 +0200
     1.3 @@ -338,10 +338,11 @@
     1.4  
     1.5  (* primitive rules *)
     1.6  
     1.7 -fun add_classrel th thy =
     1.8 +fun add_classrel raw_th thy =
     1.9    let
    1.10 +    val th = Thm.strip_shyps (Thm.transfer thy raw_th);
    1.11 +    val prop = Thm.plain_prop_of th;
    1.12      fun err () = raise THM ("add_classrel: malformed class relation", 0, [th]);
    1.13 -    val prop = Thm.plain_prop_of (Thm.transfer thy th);
    1.14      val rel = Logic.dest_classrel prop handle TERM _ => err ();
    1.15      val (c1, c2) = cert_classrel thy rel handle TYPE _ => err ();
    1.16    in
    1.17 @@ -351,10 +352,11 @@
    1.18      |> perhaps complete_arities
    1.19    end;
    1.20  
    1.21 -fun add_arity th thy =
    1.22 +fun add_arity raw_th thy =
    1.23    let
    1.24 +    val th = Thm.strip_shyps (Thm.transfer thy raw_th);
    1.25 +    val prop = Thm.plain_prop_of th;
    1.26      fun err () = raise THM ("add_arity: malformed type arity", 0, [th]);
    1.27 -    val prop = Thm.plain_prop_of (Thm.transfer thy th);
    1.28      val (t, Ss, c) = Logic.dest_arity prop handle TERM _ => err ();
    1.29      val T = Type (t, map TFree (Name.names Name.context Name.aT Ss));
    1.30      val missing_params = Sign.complete_sort thy [c]