# HG changeset patch
# User haftmann
# Date 1174077140 -3600
# Node ID 2a93fb1993021600b468c75d2d3ad66af34446b0
# Parent  052cfe1c86dc5ff66ebcd5b5bc17eff6895a706c
clarified check of defining equations

diff -r 052cfe1c86dc -r 2a93fb199302 src/Pure/Tools/codegen_func.ML
--- a/src/Pure/Tools/codegen_func.ML	Fri Mar 16 21:32:19 2007 +0100
+++ b/src/Pure/Tools/codegen_func.ML	Fri Mar 16 21:32:20 2007 +0100
@@ -88,10 +88,13 @@
             ) args [])
           then bad_thm "Repeated variables on left hand side of defining equation" thm
           else ()
-        fun no_abs (Abs _) = bad_thm "Abstraction on left hand side of defining equation" thm 
-          | no_abs (t1 $ t2) = (no_abs t1; no_abs t2)
-          | no_abs _ = ();
-        val _ = map no_abs args;
+        fun check _ (Abs _) = bad_thm
+              "Abstraction on left hand side of defining equation" thm
+          | check false (Var _) = bad_thm
+              "Variable with application on left hand side of defining equation" thm
+          | check _ (t1 $ t2) = (check false t1; check true t2)
+          | check _ _ = ();
+        val _ = map (check true) args;
       in thm end
   | NONE => bad_thm "Not a defining equation" thm;