--- a/src/HOL/Prolog/Test.thy Sat Dec 01 18:51:46 2001 +0100
+++ b/src/HOL/Prolog/Test.thy Sat Dec 01 18:52:32 2001 +0100
@@ -3,10 +3,10 @@
Test = HOHH +
types nat
-arities nat :: term
+arities nat :: type
types 'a list
-arities list :: (term) term
+arities list :: (type) type
consts Nil :: 'a list ("[]")
Cons :: 'a => 'a list => 'a list (infixr "#" 65)
@@ -20,7 +20,7 @@
"[x]" == "x#[]"
types person
-arities person :: term
+arities person :: type
consts
append :: ['a list, 'a list, 'a list] => bool