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.
generated code: raise Match instead of ERROR;
authorwenzelm
Sat, 14 Jan 2006 17:14:11 +0100
changeset 18679 cf9f1584431a
parent 18678 dd0c569fa43d
child 18680 677e2bdd75f0
generated code: raise Match instead of ERROR;
src/HOL/MicroJava/J/JListExample.thy file | annotate | diff | comparison | revisions
src/HOL/MicroJava/JVM/JVMListExample.thy file | annotate | diff | comparison | revisions
src/Pure/codegen.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/MicroJava/J/JListExample.thy	Sat Jan 14 17:14:06 2006 +0100
+++ b/src/HOL/MicroJava/J/JListExample.thy	Sat Jan 14 17:14:11 2006 +0100
@@ -72,7 +72,7 @@
   in nr 0 end;
 *}
 
-  "arbitrary" ("(raise ERROR)")
+  "arbitrary" ("(raise Match)")
   "arbitrary" :: "val" ("{* Unit *}")
   "arbitrary" :: "cname" ("\"\"")
 
--- a/src/HOL/MicroJava/JVM/JVMListExample.thy	Sat Jan 14 17:14:06 2006 +0100
+++ b/src/HOL/MicroJava/JVM/JVMListExample.thy	Sat Jan 14 17:14:11 2006 +0100
@@ -101,7 +101,7 @@
   in nr 0 end;
 *}
 
-  "arbitrary" ("(raise ERROR)")
+  "arbitrary" ("(raise Match)")
   "arbitrary" :: "val" ("{* Unit *}")
   "arbitrary" :: "cname" ("{* Object *}")
 
--- a/src/Pure/codegen.ML	Sat Jan 14 17:14:06 2006 +0100
+++ b/src/Pure/codegen.ML	Sat Jan 14 17:14:11 2006 +0100
@@ -1092,7 +1092,7 @@
       ("test",
        "fun gen_fun_type _ G i =\n\
        \  let\n\
-       \    val f = ref (fn x => raise ERROR);\n\
+       \    val f = ref (fn x => raise Match);\n\
        \    val _ = (f := (fn x =>\n\
        \      let\n\
        \        val y = G i;\n\
isabelle