# HG changeset patch
# User haftmann
# Date 1249977916 -7200
# Node ID e11cd88e6ade0a23abf2061e150ba01e05d32d22
# Parent  806d2df4d79d66cf874b80f641117b30ac9ab2f4
temporary adjustment to dubious state of eta expansion in recfun_codegen

diff -r 806d2df4d79d -r e11cd88e6ade src/HOL/Lambda/WeakNorm.thy
--- a/src/HOL/Lambda/WeakNorm.thy	Mon Aug 10 13:34:50 2009 +0200
+++ b/src/HOL/Lambda/WeakNorm.thy	Tue Aug 11 10:05:16 2009 +0200
@@ -444,7 +444,7 @@
   "default" ("(error \"default\")")
   "default :: 'a \<Rightarrow> 'b::default" ("(fn '_ => error \"default\")")
 
-code_module Norm
+(*code_module Norm
 contains
   test = "type_NF"
 
@@ -509,6 +509,6 @@
 val ct2 = @{cterm "%f x. (%x. f x x) ((%x. f x x) ((%x. f x x) ((%x. f x x) ((%x. f x x) ((%x. f x x) x)))))"};
 val (dB2, _) = Norm.type_NF (typing_of_term [] dummyf (term_of ct2));
 val ct2' = cterm_of @{theory} (term_of_dB [] (#T (rep_cterm ct2)) dB2);
-*}
+*}*)
 
 end
diff -r 806d2df4d79d -r e11cd88e6ade src/HOL/MicroJava/J/JListExample.thy
--- a/src/HOL/MicroJava/J/JListExample.thy	Mon Aug 10 13:34:50 2009 +0200
+++ b/src/HOL/MicroJava/J/JListExample.thy	Tue Aug 11 10:05:16 2009 +0200
@@ -1,12 +1,11 @@
 (*  Title:      HOL/MicroJava/J/JListExample.thy
-    ID:         $Id$
     Author:     Stefan Berghofer
 *)
 
 header {* \isaheader{Example for generating executable code from Java semantics} *}
 
 theory JListExample
-imports Eval SystemClasses
+imports Eval
 begin
 
 ML {* Syntax.ambiguity_level := 100000 *}
diff -r 806d2df4d79d -r e11cd88e6ade src/HOL/MicroJava/J/State.thy
--- a/src/HOL/MicroJava/J/State.thy	Mon Aug 10 13:34:50 2009 +0200
+++ b/src/HOL/MicroJava/J/State.thy	Tue Aug 11 10:05:16 2009 +0200
@@ -1,12 +1,13 @@
 (*  Title:      HOL/MicroJava/J/State.thy
-    ID:         $Id$
     Author:     David von Oheimb
     Copyright   1999 Technische Universitaet Muenchen
 *)
 
 header {* \isaheader{Program State} *}
 
-theory State imports TypeRel Value begin
+theory State
+imports TypeRel Value
+begin
 
 types 
   fields' = "(vname \<times> cname \<rightharpoonup> val)"  -- "field name, defining class, value"
@@ -19,7 +20,10 @@
 
   init_vars :: "('a \<times> ty) list => ('a \<rightharpoonup> val)"
  "init_vars == map_of o map (\<lambda>(n,T). (n,default_val T))"
-  
+
+lemma [code] (*manual eta expansion*):
+  "init_vars xs = map_of (map (\<lambda>(n, T). (n, default_val T)) xs)"
+  by (simp add: init_vars_def)
 
 types aheap  = "loc \<rightharpoonup> obj"    -- {* "@{text heap}" used in a translation below *}
       locals = "vname \<rightharpoonup> val"  -- "simple state, i.e. variable contents"
diff -r 806d2df4d79d -r e11cd88e6ade src/HOL/MicroJava/JVM/JVMListExample.thy
--- a/src/HOL/MicroJava/JVM/JVMListExample.thy	Mon Aug 10 13:34:50 2009 +0200
+++ b/src/HOL/MicroJava/JVM/JVMListExample.thy	Tue Aug 11 10:05:16 2009 +0200
@@ -1,11 +1,12 @@
 (*  Title:      HOL/MicroJava/JVM/JVMListExample.thy
-    ID:         $Id$
     Author:     Stefan Berghofer
 *)
 
 header {* \isaheader{Example for generating executable code from JVM semantics}\label{sec:JVMListExample} *}
 
-theory JVMListExample imports "../J/SystemClasses" JVMExec begin
+theory JVMListExample
+imports "../J/SystemClasses" JVMExec
+begin
 
 consts
   list_nam :: cnam