adjusted definition of defining equation
authorhaftmann
Tue Mar 20 08:27:20 2007 +0100 (2007-03-20)
changeset 22475bd3378255cc8
parent 22474 ecdaec8cf13a
child 22476 088e141084a6
adjusted definition of defining equation
src/Pure/Tools/codegen_func.ML
     1.1 --- a/src/Pure/Tools/codegen_func.ML	Tue Mar 20 08:27:19 2007 +0100
     1.2 +++ b/src/Pure/Tools/codegen_func.ML	Tue Mar 20 08:27:20 2007 +0100
     1.3 @@ -90,11 +90,15 @@
     1.4            else ()
     1.5          fun check _ (Abs _) = bad_thm
     1.6                "Abstraction on left hand side of defining equation" thm
     1.7 -          | check false (Var _) = bad_thm
     1.8 +          | check 0 (Var _) = ()
     1.9 +          | check _ (Var _) = bad_thm
    1.10                "Variable with application on left hand side of defining equation" thm
    1.11 -          | check _ (t1 $ t2) = (check false t1; check true t2)
    1.12 -          | check _ _ = ();
    1.13 -        val _ = map (check true) args;
    1.14 +          | check n (t1 $ t2) = (check (n+1) t1; check 0 t2)
    1.15 +          | check n (Const (_, ty)) = if n <> (length o fst o strip_type) ty
    1.16 +              then bad_thm
    1.17 +                ("Partially applied constant on left hand side of defining equation") thm
    1.18 +              else ();
    1.19 +        val _ = map (check 0) args;
    1.20        in thm end
    1.21    | NONE => bad_thm "Not a defining equation" thm;
    1.22