--- a/src/HOL/Tools/TFL/usyntax.ML	Sat Mar 22 18:16:54 2014 +0100
+++ b/src/HOL/Tools/TFL/usyntax.ML	Sat Mar 22 18:19:57 2014 +0100
@@ -104,7 +104,7 @@
  *
  *---------------------------------------------------------------------------*)
 val mk_prim_vartype = TVar;
-fun mk_vartype s = mk_prim_vartype ((s, 0), HOLogic.typeS);
+fun mk_vartype s = mk_prim_vartype ((s, 0), @{sort type});
 
 (* But internally, it's useful *)
 fun dest_vtype (TVar x) = x