src/Pure/Thy/export_theory.ML

         val used_typargs = fold (Name.declare o #1) typargs used;
         val sorts = Name.invent used_typargs Name.aT (length extra_shyps) ~~ extra_shyps;
       in ((sorts @ typargs, args, prop), proof) end;
 
     fun standard_prop_of thm =
-      standard_prop Name.context (Thm.extra_shyps thm) (Thm.full_prop_of thm);
+      standard_prop Name.context (Sortset.dest (Thm.extra_shyps thm)) (Thm.full_prop_of thm);
 
     val encode_prop =
       let open XML.Encode Term_XML.Encode
       in triple (list (pair string sort)) (list (pair string typ)) encode_term end;