HOLogic.typeS;
authorwenzelm
Mon Dec 03 11:46:13 2001 +0100 (2001-12-03)
changeset 1234024d31d47af1a
parent 12339 f0b62ad4e1a6
child 12341 08afd1003151
HOLogic.typeS;
TFL/thry.ML
TFL/usyntax.ML
     1.1 --- a/TFL/thry.ML	Sat Dec 01 18:55:41 2001 +0100
     1.2 +++ b/TFL/thry.ML	Mon Dec 03 11:46:13 2001 +0100
     1.3 @@ -26,7 +26,7 @@
     1.4   *    Matching
     1.5   *---------------------------------------------------------------------------*)
     1.6  
     1.7 -local fun tybind (x,y) = (TVar (x, HOLogic.termS) , y)
     1.8 +local fun tybind (x,y) = (TVar (x, HOLogic.typeS) , y)
     1.9        fun tmbind (x,y) = (Var  (x, Term.type_of y), y)
    1.10  in
    1.11   fun match_term thry pat ob =
     2.1 --- a/TFL/usyntax.ML	Sat Dec 01 18:55:41 2001 +0100
     2.2 +++ b/TFL/usyntax.ML	Mon Dec 03 11:46:13 2001 +0100
     2.3 @@ -106,7 +106,7 @@
     2.4   *
     2.5   *---------------------------------------------------------------------------*)
     2.6  val mk_prim_vartype = TVar;
     2.7 -fun mk_vartype s = mk_prim_vartype ((s, 0), HOLogic.termS);
     2.8 +fun mk_vartype s = mk_prim_vartype ((s, 0), HOLogic.typeS);
     2.9  
    2.10  (* But internally, it's useful *)
    2.11  fun dest_vtype (TVar x) = x