# HG changeset patch
# User haftmann
# Date 1174375640 -3600
# Node ID bd3378255cc881bbbec1d3285cb47b3c374e170a
# Parent  ecdaec8cf13acb07e521ad07753730faaad2203d
adjusted definition of defining equation

diff -r ecdaec8cf13a -r bd3378255cc8 src/Pure/Tools/codegen_func.ML
--- a/src/Pure/Tools/codegen_func.ML	Tue Mar 20 08:27:19 2007 +0100
+++ b/src/Pure/Tools/codegen_func.ML	Tue Mar 20 08:27:20 2007 +0100
@@ -90,11 +90,15 @@
           else ()
         fun check _ (Abs _) = bad_thm
               "Abstraction on left hand side of defining equation" thm
-          | check false (Var _) = bad_thm
+          | check 0 (Var _) = ()
+          | check _ (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;
+          | check n (t1 $ t2) = (check (n+1) t1; check 0 t2)
+          | check n (Const (_, ty)) = if n <> (length o fst o strip_type) ty
+              then bad_thm
+                ("Partially applied constant on left hand side of defining equation") thm
+              else ();
+        val _ = map (check 0) args;
       in thm end
   | NONE => bad_thm "Not a defining equation" thm;