# HG changeset patch
# User berghofe
# Date 1188318113 -7200
# Node ID 62b96cf2bebbc274cc9b2b64667a16aee011f6d4
# Parent  fd114392bca9e5b923477eb3452ea2f3f6c3e427
Code generator now uses sequences with depth limit.

diff -r fd114392bca9 -r 62b96cf2bebb src/HOL/MicroJava/J/JListExample.thy
--- a/src/HOL/MicroJava/J/JListExample.thy	Tue Aug 28 18:20:11 2007 +0200
+++ b/src/HOL/MicroJava/J/JListExample.thy	Tue Aug 28 18:21:53 2007 +0200
@@ -109,7 +109,7 @@
 
 ML {*
 
-val SOME ((_, (heap, locs)), _) = Seq.pull J.test;
+val SOME ((_, (heap, locs)), _) = DSeq.pull J.test;
 locs J.l1_name;
 locs J.l2_name;
 locs J.l3_name;