# HG changeset patch
# User haftmann
# Date 1162560164 -3600
# Node ID b379fdc3a3bdd042540a5cb65bacebd2db26c683
# Parent  dae0416fddfdc85d7d0b30602c284ed4840de1c5
tightened notion of function equations

diff -r dae0416fddfd -r b379fdc3a3bd src/Pure/Tools/codegen_data.ML
--- a/src/Pure/Tools/codegen_data.ML	Fri Nov 03 14:22:43 2006 +0100
+++ b/src/Pure/Tools/codegen_data.ML	Fri Nov 03 14:22:44 2006 +0100
@@ -163,7 +163,10 @@
       let
         val _ =
           if has_duplicates (op =)
-            ((fold o fold_aterms) (fn Var (v, _) => cons v | _ => I) args [])
+            ((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 ()
         val is_classop = (is_some o AxClass.class_of_param thy) c;
@@ -647,7 +650,7 @@
 
 fun del_func thm thy =
   let
-    val thms = setmp strict_functyp false (mk_func thy) thm;
+    val thms = mk_func thy thm;
     val cs = map fst thms;
   in
     map_exec_purge (SOME cs) (map_funcs
@@ -852,5 +855,3 @@
 open CodegenData;
 
 end;
-
-set Toplevel.debug;