# HG changeset patch
# User haftmann
# Date 1186758606 -7200
# Node ID 348e982c694b70ea06f2ad0bbc0bae0a8c24e434
# Parent  a5c95bbeb31dccccad5b5faaf138e6dcf6e87c65
dropped code generator setup garbage

diff -r a5c95bbeb31d -r 348e982c694b src/HOL/MicroJava/JVM/JVMListExample.thy
--- a/src/HOL/MicroJava/JVM/JVMListExample.thy	Fri Aug 10 17:10:05 2007 +0200
+++ b/src/HOL/MicroJava/JVM/JVMListExample.thy	Fri Aug 10 17:10:06 2007 +0200
@@ -112,60 +112,6 @@
   "val_nam" ("\"val\"")
   "next_nam" ("\"next\"")
 
-code_type cnam and vnam and mname and loc_
-  (SML "string" and "string" and "string" and "IntInf.int")
-
-instance cnam :: eq
-  and cname :: eq
-  and vname :: eq
-  and mname :: eq
-  and ty :: eq
-  and val :: eq
-  and instr :: eq ..
-
-definition
-  arbitrary_val :: val where
-  [symmetric, code inline]: "arbitrary_val = arbitrary"
-definition
-  arbitrary_cname :: cname where
-  [symmetric, code inline]: "arbitrary_cname = arbitrary"
-
-definition "unit' = Unit"
-definition "object' = Object"
-
-code_axioms
-  arbitrary_val \<equiv> unit'
-  arbitrary_cname \<equiv> object'
-
-code_const list_nam and test_nam and append_name and makelist_name and val_nam and next_nam
-  (SML "\"list\"" and "\"test\"" and "\"append\""
-    and "\"makelist\"" and "\"val\"" and "\"next\"")
-
-axiomatization
-  incr_loc :: "loc_ \<Rightarrow> loc_"
-  and zero_loc :: "loc_"
-
-code_const incr_loc and zero_loc
-  (SML "(op +)/ (_, 1)" and "0")
-
-axiomatization
-  test_loc :: "(loc_ \<Rightarrow> bool) \<Rightarrow> (loc_ \<Rightarrow> 'a) \<Rightarrow> loc_ \<Rightarrow> 'a" where
-  "test_loc p v l = (if p l then v l else test_loc p v (incr l))"
-
-definition
-  new_addr' :: "(loc \<Rightarrow> (cname \<times> (vname \<times> cname \<Rightarrow> val option)) option) \<Rightarrow> loc \<times> val option" where
-  "new_addr' hp =
-    test_loc (\<lambda>i. hp (Loc i) = None) (\<lambda>i. (Loc i, None)) zero_loc"
-
-lemma [code func]:
-  "wf_class = wf_class" ..
-
-code_const
-  wf_class (SML "(fn `_ => true)")
-
-code_axioms
-  new_Addr \<equiv> new_addr'
-
 definition
   "test = exec (E, start_state E test_name makelist_name)"
 
@@ -174,7 +120,8 @@
 
 code_module JVM
 contains
-  test = "exec (E, start_state E test_name makelist_name)"
+  exec = exec
+  test = test
 
 ML {*
 JVM.test;