src/HOL/Tools/TFL/usyntax.ML
changeset 56254 a2dd9200854d
parent 55414 eab03e9cee8a
     1.1 --- a/src/HOL/Tools/TFL/usyntax.ML	Sat Mar 22 18:16:54 2014 +0100
     1.2 +++ b/src/HOL/Tools/TFL/usyntax.ML	Sat Mar 22 18:19:57 2014 +0100
     1.3 @@ -104,7 +104,7 @@
     1.4   *
     1.5   *---------------------------------------------------------------------------*)
     1.6  val mk_prim_vartype = TVar;
     1.7 -fun mk_vartype s = mk_prim_vartype ((s, 0), HOLogic.typeS);
     1.8 +fun mk_vartype s = mk_prim_vartype ((s, 0), @{sort type});
     1.9  
    1.10  (* But internally, it's useful *)
    1.11  fun dest_vtype (TVar x) = x