src/Pure/axclass.ML

   end;
 
 
 (* primitive rules *)
 
-fun add_classrel th thy =
-  let
+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
     thy
     |> Sign.primitive_classrel (c1, c2)
     |> put_classrel ((c1, c2), Thm.close_derivation (Drule.unconstrainTs th))
     |> perhaps complete_arities
   end;
 
-fun add_arity th thy =
-  let
+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]
       |> maps (these o Option.map #params o try (get_info thy))
       |> filter_out (fn (const, _) => can (get_inst_param thy) (const, t))