# HG changeset patch
# User wenzelm
# Date 1137255251 -3600
# Node ID cf9f1584431aae922133a749933d03977af943e1
# Parent  dd0c569fa43d641dfe822fd79fd1d8c99d157c95
generated code: raise Match instead of ERROR;

diff -r dd0c569fa43d -r cf9f1584431a src/HOL/MicroJava/J/JListExample.thy
--- 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" ("\"\"")
 
diff -r dd0c569fa43d -r cf9f1584431a src/HOL/MicroJava/JVM/JVMListExample.thy
--- 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 *}")
 
diff -r dd0c569fa43d -r cf9f1584431a src/Pure/codegen.ML
--- 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\