diff -r 1f00494e37a5 -r 5d909faf0e04 src/HOL/MiniML/MiniML.thy
--- a/src/HOL/MiniML/MiniML.thy	Fri Dec 08 13:22:55 1995 +0100
+++ b/src/HOL/MiniML/MiniML.thy	Fri Dec 08 19:48:15 1995 +0100
@@ -14,9 +14,9 @@
 
 (* type inference rules *)
 consts
-	has_type :: "(type_expr list * expr * type_expr)set"
+	has_type :: "(typ list * expr * typ)set"
 syntax
-        "@has_type" :: [type_expr list, expr, type_expr] => bool
+        "@has_type" :: [typ list, expr, typ] => bool
                        ("((_) |-/ (_) :: (_))" 60)
 translations 
         "a |- e :: t" == "(a,e,t):has_type"
@@ -24,8 +24,8 @@
 inductive "has_type"
 intrs
 	VarI "[| n < length a |] ==> a |- Var n :: nth n a"
-	AbsI "[| t1#a |- e :: t2 |] ==> a |- Abs e :: Fun t1 t2"
-	AppI "[| a |- e1 :: Fun t2 t1; a |- e2 :: t2 |] 
+	AbsI "[| t1#a |- e :: t2 |] ==> a |- Abs e :: t1 -> t2"
+	AppI "[| a |- e1 :: t2 -> t1; a |- e2 :: t2 |] 
      	      ==> a |- App e1 e2 :: t1"
 
 end