# HG changeset patch
# User wenzelm
# Date 1149638357 -7200
# Node ID d0318ae1141c53a70d04e51457e93e042a9dc195
# Parent  aa2581752afbd2baec8f5ce7649f3004c1ef0151
tuned;

diff -r aa2581752afb -r d0318ae1141c src/HOLCF/IOA/meta_theory/Seq.thy
--- a/src/HOLCF/IOA/meta_theory/Seq.thy	Wed Jun 07 01:51:22 2006 +0200
+++ b/src/HOLCF/IOA/meta_theory/Seq.thy	Wed Jun 07 01:59:17 2006 +0200
@@ -114,27 +114,10 @@
     sfinite_0:  "nil:sfinite"
     sfinite_n:  "[|tr:sfinite;a~=UU|] ==> (a##tr) : sfinite"
 
-ML {* use_legacy_bindings (the_context ()) *}
-ML {*
-structure seq =
-struct
-  open seq
-  val injects = [injects]
-  val inverts = [inverts]
-  val finites = [finites]
-  val take_lemmas = [take_lemmas]
-end
-structure sfinite =
-struct
-  open sfinite
-  val elim = elims
-  val elims = [elims]
-end
-*}
-
 declare sfinite.intros [simp]
 declare seq.rews [simp]
 
+
 subsection {* recursive equations of operators *}
 
 subsubsection {* smap *}
@@ -508,6 +491,4 @@
 apply simp
 done
 
-ML {* use_legacy_bindings (the_context ()) *}
-
 end