diff -r 84a6d701e36f -r 98c00ee9e786 src/Tools/Code/code_thingol.ML
--- a/src/Tools/Code/code_thingol.ML	Tue Aug 11 10:05:53 2009 +0200
+++ b/src/Tools/Code/code_thingol.ML	Tue Aug 11 10:43:43 2009 +0200
@@ -79,7 +79,8 @@
   val is_cons: program -> string -> bool
   val contr_classparam_typs: program -> string -> itype option list
 
-  val clean_thms: theory -> typ -> thm list -> thm list
+  val expand_eta: theory -> int -> thm -> thm
+  val clean_thms: theory -> thm list -> thm list
   val read_const_exprs: theory -> string list -> string list * string list
   val consts_program: theory -> string list -> string list * (naming * program)
   val cached_program: theory -> naming * program
@@ -403,12 +404,6 @@
     val k = fold (curry Int.max o num_args_of o Thm.prop_of) thms 0;
   in map (expand_eta thy k) thms end;
 
-fun avoid_value thy ty [thm] =
-      if null (Term.add_tfreesT ty []) orelse (null o fst o strip_type) ty
-      then [thm]
-      else [expand_eta thy 1 thm]
-  | avoid_value thy _ thms = thms;
-
 fun mk_desymbolization pre post mk vs =
   let
     val names = map (pre o fst o fst) vs
@@ -434,8 +429,7 @@
 
 fun desymbolize_all_vars thy = desymbolize_tvars thy #> map (desymbolize_vars thy);
 
-fun clean_thms thy ty =
-  same_arity thy #> avoid_value thy ty #> desymbolize_all_vars thy;
+fun clean_thms thy = same_arity thy #> desymbolize_all_vars thy;
 
 
 (** statements, abstract programs **)
@@ -563,7 +557,7 @@
     fun stmt_fun ((vs, ty), eqns) =
       fold_map (translate_tyvar_sort thy algbr funcgr) vs
       ##>> translate_typ thy algbr funcgr ty
-      ##>> fold_map (translate_eqn thy algbr funcgr) (burrow_fst (clean_thms thy ty) eqns)
+      ##>> fold_map (translate_eqn thy algbr funcgr) (burrow_fst (clean_thms thy) eqns)
       #>> (fn info => Fun (c, info));
     val stmt_const = case Code.get_datatype_of_constr thy c
      of SOME tyco => stmt_datatypecons tyco