src/HOL/MiniML/Type.thy

--- a/src/HOL/MiniML/Type.thy	Sun Mar 24 18:36:28 1996 +0100
+++ b/src/HOL/MiniML/Type.thy	Mon Mar 25 08:46:02 1996 +0100
@@ -36,9 +36,10 @@
 consts
         app_subst :: [subst, 'a::type_struct] => 'a::type_struct ("$")
 
-rules
-        app_subst_TVar  "$ s (TVar n) = s n" 
-        app_subst_Fun   "$ s (t1 -> t2) = ($ s t1) -> ($ s t2)" 
+primrec app_subst typ
+  app_subst_TVar  "$ s (TVar n) = s n" 
+  app_subst_Fun   "$ s (t1 -> t2) = ($ s t1) -> ($ s t2)" 
+
 defs
         app_subst_list  "$ s == map ($ s)"