# HG changeset patch
# User wenzelm
# Date 877344422 -7200
# Node ID dca1bce88ec84e6307e6f90f2e08331e3c654a4d
# Parent  d52a49a7d8f3a11c2b454821f36be1882ad9da99
replaced ops by consts;

diff -r d52a49a7d8f3 -r dca1bce88ec8 src/HOLCF/IOA/meta_theory/Sequence.thy
--- a/src/HOLCF/IOA/meta_theory/Sequence.thy	Mon Oct 20 12:45:51 1997 +0200
+++ b/src/HOLCF/IOA/meta_theory/Sequence.thy	Mon Oct 20 12:47:02 1997 +0200
@@ -13,7 +13,7 @@
 
 types 'a Seq = ('a::term lift)seq
 
-ops curried
+consts
 
   Cons             ::"'a            => 'a Seq -> 'a Seq"
   Filter           ::"('a => bool)  => 'a Seq -> 'a Seq"