diff -r 2fd82cec17d4 -r fe30812f5b5e src/HOL/MiniML/Type.thy
--- a/src/HOL/MiniML/Type.thy	Wed Mar 06 14:12:24 1996 +0100
+++ b/src/HOL/MiniML/Type.thy	Wed Mar 06 14:19:39 1996 +0100
@@ -28,10 +28,9 @@
 (* substitutions *)
 
 (* identity *)
-consts
+constdefs
         id_subst :: subst
-defs
-        id_subst_def "id_subst == (%n.TVar n)"
+        "id_subst == (%n.TVar n)"
 
 (* extension of substitution to type structures *)
 consts
@@ -54,16 +53,14 @@
         free_tv_Cons    "free_tv (x#l) = (free_tv x) Un (free_tv l)"
 
 (* domain of a substitution *)
-consts
+constdefs
         dom :: subst => nat set
-defs
-        dom_def         "dom s == {n. s n ~= TVar n}" 
+        "dom s == {n. s n ~= TVar n}" 
 
 (* codomain of a substitutions: the introduced variables *)
-consts
+constdefs
      cod :: subst => nat set
-defs
-        cod_def         "cod s == (UN m:dom s. free_tv (s m))"
+     "cod s == (UN m:dom s. free_tv (s m))"
 
 defs
         free_tv_subst   "free_tv s == (dom s) Un (cod s)"
@@ -71,10 +68,9 @@
 (* new_tv s n computes whether n is a new type variable w.r.t. a type 
    structure s, i.e. whether n is greater than any type variable 
    occuring in the type structure *)
-consts
+constdefs
         new_tv :: [nat,'a::type_struct] => bool
-defs
-        new_tv_def      "new_tv n ts == ! m. m:free_tv ts --> m<n"
+        "new_tv n ts == ! m. m:free_tv ts --> m<n"
 
 (* unification algorithm mgu *)
 consts