Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Code generator now uses sequences with depth limit.
authorberghofe
Tue, 28 Aug 2007 18:21:53 +0200
changeset 24460 62b96cf2bebb
parent 24459 fd114392bca9
child 24461 bbff04c027ec
Code generator now uses sequences with depth limit.
src/HOL/MicroJava/J/JListExample.thy file | annotate | diff | comparison | revisions 
--- 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;
isabelle