# HG changeset patch
# User haftmann
# Date 1249980371 -7200
# Node ID bc1e123295f5d484d8da13564d0b4d4f58fb1b3f
# Parent  98c00ee9e78609c048eb3a5a8d13cc0ea372ca65
dropped temporary adjustments to non-working eta expansion in recfun_codegen.ML

diff -r 98c00ee9e786 -r bc1e123295f5 src/HOL/Lambda/WeakNorm.thy
--- a/src/HOL/Lambda/WeakNorm.thy	Tue Aug 11 10:43:43 2009 +0200
+++ b/src/HOL/Lambda/WeakNorm.thy	Tue Aug 11 10:46:11 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 98c00ee9e786 -r bc1e123295f5 src/HOL/MicroJava/J/State.thy
--- a/src/HOL/MicroJava/J/State.thy	Tue Aug 11 10:43:43 2009 +0200
+++ b/src/HOL/MicroJava/J/State.thy	Tue Aug 11 10:46:11 2009 +0200
@@ -21,10 +21,6 @@
   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"