src/ZF/ex/LList.ML

 
 structure LList = CoDatatype_Fun
  (val thy        = QUniv.thy
   val thy_name   = "LList"
   val rec_specs  = [("llist", "quniv(A)",
-                      [(["LNil"],   "i",NoSyn), 
-                       (["LCons"],  "[i,i]=>i",NoSyn)])]
+                      [(["LNil"],   "i",	NoSyn), 
+                       (["LCons"],  "[i,i]=>i",	NoSyn)])]
   val rec_styp   = "i=>i"
   val sintrs     = ["LNil : llist(A)",
                     "[| a: A;  l: llist(A) |] ==> LCons(a,l) : llist(A)"]
   val monos      = []
   val type_intrs = codatatype_intrs