# HG changeset patch
# User clasohm
# Date 826714575 -3600
# Node ID 4118fb066ba95a0b9683440b5279cf762c609990
# Parent  5a63ab90ee8ab88787b3570bdc0b715a540a479b
replaced rules by primrec section

diff -r 5a63ab90ee8a -r 4118fb066ba9 src/HOL/MiniML/Type.thy
--- a/src/HOL/MiniML/Type.thy	Wed Mar 13 11:55:25 1996 +0100
+++ b/src/HOL/MiniML/Type.thy	Wed Mar 13 11:56:15 1996 +0100
@@ -46,11 +46,13 @@
 consts
         free_tv :: ['a::type_struct] => nat set
 
-rules
-        free_tv_TVar    "free_tv (TVar m) = {m}"
-        free_tv_Fun     "free_tv (t1 -> t2) = (free_tv t1) Un (free_tv t2)"
-        free_tv_Nil     "free_tv [] = {}"
-        free_tv_Cons    "free_tv (x#l) = (free_tv x) Un (free_tv l)"
+primrec free_tv typ
+  free_tv_TVar    "free_tv (TVar m) = {m}"
+  free_tv_Fun     "free_tv (t1 -> t2) = (free_tv t1) Un (free_tv t2)"
+
+primrec free_tv List.list
+  free_tv_Nil     "free_tv [] = {}"
+  free_tv_Cons    "free_tv (x#l) = (free_tv x) Un (free_tv l)"
 
 (* domain of a substitution *)
 constdefs
@@ -59,8 +61,8 @@
 
 (* codomain of a substitutions: the introduced variables *)
 constdefs
-     cod :: subst => nat set
-     "cod s == (UN m:dom s. free_tv (s m))"
+        cod :: subst => nat set
+        "cod s == (UN m:dom s. free_tv (s m))"
 
 defs
         free_tv_subst   "free_tv s == (dom s) Un (cod s)"