diff -r b33b42211bbf -r 188826f1ccdb Nominal/nominal_function.ML
--- a/Nominal/nominal_function.ML	Thu Mar 13 09:30:26 2014 +0000
+++ b/Nominal/nominal_function.ML	Mon Mar 24 15:31:17 2014 +0000
@@ -205,7 +205,7 @@
   end
 
 val add_nominal_function =
-  gen_add_nominal_function false Specification.check_spec (Type_Infer.anyT HOLogic.typeS)
+  gen_add_nominal_function false Specification.check_spec (Type_Infer.anyT @{sort type})
 fun add_nominal_function_cmd a b c d int = 
   gen_add_nominal_function int Specification.read_spec "_::type" a b c d
 
@@ -220,7 +220,7 @@
   end
 
 val nominal_function =
-  gen_nominal_function false Specification.check_spec (Type_Infer.anyT HOLogic.typeS)
+  gen_nominal_function false Specification.check_spec (Type_Infer.anyT @{sort type})
 fun nominal_function_cmd a b c int = 
   gen_nominal_function int Specification.read_spec "_::type" a b c