--- 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;