src/Pure/Tools/codegen_func.ML
changeset 22462 2a93fb199302
parent 22211 e2b5f3d24a17
child 22475 bd3378255cc8
     1.1 --- a/src/Pure/Tools/codegen_func.ML	Fri Mar 16 21:32:19 2007 +0100
     1.2 +++ b/src/Pure/Tools/codegen_func.ML	Fri Mar 16 21:32:20 2007 +0100
     1.3 @@ -88,10 +88,13 @@
     1.4              ) args [])
     1.5            then bad_thm "Repeated variables on left hand side of defining equation" thm
     1.6            else ()
     1.7 -        fun no_abs (Abs _) = bad_thm "Abstraction on left hand side of defining equation" thm 
     1.8 -          | no_abs (t1 $ t2) = (no_abs t1; no_abs t2)
     1.9 -          | no_abs _ = ();
    1.10 -        val _ = map no_abs args;
    1.11 +        fun check _ (Abs _) = bad_thm
    1.12 +              "Abstraction on left hand side of defining equation" thm
    1.13 +          | check false (Var _) = bad_thm
    1.14 +              "Variable with application on left hand side of defining equation" thm
    1.15 +          | check _ (t1 $ t2) = (check false t1; check true t2)
    1.16 +          | check _ _ = ();
    1.17 +        val _ = map (check true) args;
    1.18        in thm end
    1.19    | NONE => bad_thm "Not a defining equation" thm;
    1.20