src/Pure/axclass.ML

--- a/src/Pure/axclass.ML	Wed Aug 30 14:04:39 1995 +0200
+++ b/src/Pure/axclass.ML	Fri Sep 01 13:08:55 1995 +0200
@@ -121,11 +121,11 @@
   let
     fun err msg = raise THM ("prep_thm_axm: " ^ msg, 0, [thm]);
 
-    val {sign, shyps, hyps, prop, ...} = rep_thm thm;
+    val {sign, hyps, prop, ...} = rep_thm thm;
   in
     if not (Sign.subsig (sign, sign_of thy)) then
       err "theorem not of same theory"
-    else if not (null shyps) orelse not (null hyps) then
+    else if not (null (extra_shyps thm)) orelse not (null hyps) then
       err "theorem may not contain hypotheses"
     else prop
   end;