# HG changeset patch
# User haftmann
# Date 1167915698 -3600
# Node ID e83f3b0988e66f72a230906e9708266e5c92fb22
# Parent  29d5cdd1cc03984b7846db361abc09e0217876c9
clarified code

diff -r 29d5cdd1cc03 -r e83f3b0988e6 src/Pure/Tools/codegen_data.ML
--- a/src/Pure/Tools/codegen_data.ML	Thu Jan 04 14:01:37 2007 +0100
+++ b/src/Pure/Tools/codegen_data.ML	Thu Jan 04 14:01:38 2007 +0100
@@ -162,11 +162,14 @@
         val _ =
           if has_duplicates (op =)
             ((fold o fold_aterms) (fn Var (v, _) => cons v
-              | Abs _ => bad_thm "Abstraction on left hand side of function equation" thm
               | _ => I
             ) args [])
           then bad_thm "Repeated variables on left hand side of function equation" thm
           else ()
+        fun no_abs (Abs _) = bad_thm "Abstraction on left hand side of function equation" thm 
+          | no_abs (t1 $ t2) = (no_abs t1; no_abs t2)
+          | no_abs _ = ();
+        val _ = map no_abs args;
         val is_classop = (is_some o AxClass.class_of_param thy) c;
         val const = CodegenConsts.norm_of_typ thy c_ty;
         val ty_decl = CodegenConsts.disc_typ_of_const thy