--- a/src/HOL/Nominal/nominal_thmdecls.ML Tue Aug 14 23:22:49 2007 +0200
+++ b/src/HOL/Nominal/nominal_thmdecls.ML Tue Aug 14 23:22:51 2007 +0200
@@ -144,7 +144,7 @@
(* FIXME: this should be an operation the library *)
val class_name = (NameSpace.map_base (fn s => "pt_"^s) tyatm)
in
- if (Type.of_sort (Sign.tsig_of thy) (ty,[class_name]))
+ if (Sign.of_sort thy (ty,[class_name]))
then [(pi,typi)]
else raise
EQVT_FORM ("Could not find any permutation or an argument is not an instance of "^class_name)