--- a/TFL/thry.ML Sat Dec 01 18:55:41 2001 +0100
+++ b/TFL/thry.ML Mon Dec 03 11:46:13 2001 +0100
@@ -26,7 +26,7 @@
* Matching
*---------------------------------------------------------------------------*)
-local fun tybind (x,y) = (TVar (x, HOLogic.termS) , y)
+local fun tybind (x,y) = (TVar (x, HOLogic.typeS) , y)
fun tmbind (x,y) = (Var (x, Term.type_of y), y)
in
fun match_term thry pat ob =
--- a/TFL/usyntax.ML Sat Dec 01 18:55:41 2001 +0100
+++ b/TFL/usyntax.ML Mon Dec 03 11:46:13 2001 +0100
@@ -106,7 +106,7 @@
*
*---------------------------------------------------------------------------*)
val mk_prim_vartype = TVar;
-fun mk_vartype s = mk_prim_vartype ((s, 0), HOLogic.termS);
+fun mk_vartype s = mk_prim_vartype ((s, 0), HOLogic.typeS);
(* But internally, it's useful *)
fun dest_vtype (TVar x) = x