src/ZF/List.ML

--- a/src/ZF/List.ML	Thu Jul 21 16:51:26 1994 +0200
+++ b/src/ZF/List.ML	Tue Jul 26 13:21:20 1994 +0200
@@ -10,8 +10,8 @@
  (val thy        = Univ.thy
   val thy_name   = "List"
   val rec_specs  = [("list", "univ(A)",
-                      [(["Nil"],    "i", NoSyn), 
-                       (["Cons"],   "[i,i]=>i", NoSyn)])]
+                      [(["Nil"],    "i", 	NoSyn), 
+                       (["Cons"],   "[i,i]=>i",	NoSyn)])]
   val rec_styp   = "i=>i"
   val sintrs     = ["Nil : list(A)",
                     "[| a: A;  l: list(A) |] ==> Cons(a,l) : list(A)"]