# HG changeset patch
# User wenzelm
# Date 1246919374 -7200
# Node ID ea8c8bf47ce33e160825e555b6266266fcc98b26
# Parent  7daee3bed3afbd40b0b4d70235c1cfd586d3e574
add_classrel/arity: strip_shyps of stored result;

diff -r 7daee3bed3af -r ea8c8bf47ce3 src/Pure/axclass.ML
--- a/src/Pure/axclass.ML	Mon Jul 06 22:42:27 2009 +0200
+++ b/src/Pure/axclass.ML	Tue Jul 07 00:29:34 2009 +0200
@@ -338,10 +338,11 @@
 
 (* primitive rules *)
 
-fun add_classrel th thy =
+fun add_classrel raw_th thy =
   let
+    val th = Thm.strip_shyps (Thm.transfer thy raw_th);
+    val prop = Thm.plain_prop_of th;
     fun err () = raise THM ("add_classrel: malformed class relation", 0, [th]);
-    val prop = Thm.plain_prop_of (Thm.transfer thy th);
     val rel = Logic.dest_classrel prop handle TERM _ => err ();
     val (c1, c2) = cert_classrel thy rel handle TYPE _ => err ();
   in
@@ -351,10 +352,11 @@
     |> perhaps complete_arities
   end;
 
-fun add_arity th thy =
+fun add_arity raw_th thy =
   let
+    val th = Thm.strip_shyps (Thm.transfer thy raw_th);
+    val prop = Thm.plain_prop_of th;
     fun err () = raise THM ("add_arity: malformed type arity", 0, [th]);
-    val prop = Thm.plain_prop_of (Thm.transfer thy th);
     val (t, Ss, c) = Logic.dest_arity prop handle TERM _ => err ();
     val T = Type (t, map TFree (Name.names Name.context Name.aT Ss));
     val missing_params = Sign.complete_sort thy [c]