1.1 --- a/TFL/usyntax.ML	Sat Dec 01 18:55:41 2001 +0100
     1.2 +++ b/TFL/usyntax.ML	Mon Dec 03 11:46:13 2001 +0100
     1.3 @@ -106,7 +106,7 @@
     1.4   *
     1.5   *---------------------------------------------------------------------------*)
     1.6  val mk_prim_vartype = TVar;
     1.7 -fun mk_vartype s = mk_prim_vartype ((s, 0), HOLogic.termS);
     1.8 +fun mk_vartype s = mk_prim_vartype ((s, 0), HOLogic.typeS);
     1.9  
    1.10  (* But internally, it's useful *)
    1.11  fun dest_vtype (TVar x) = x