--- a/src/Pure/Isar/specification.ML Fri Aug 10 17:04:24 2007 +0200
+++ b/src/Pure/Isar/specification.ML Fri Aug 10 17:04:34 2007 +0200
@@ -130,7 +130,7 @@
|> LocalTheory.def Thm.definitionK ((x, mx), ((name ^ "_raw", []), rhs));
val ((b, [th']), lthy3) = lthy2
|> LocalTheory.note Thm.definitionK
- ((name, CodegenData.add_func_attr false :: atts), [prove lthy2 th]);
+ ((name, Code.add_func_attr false :: atts), [prove lthy2 th]);
val lhs' = Morphism.term (LocalTheory.target_morphism lthy3) lhs;
val _ = print_consts lthy3 (member (op =) (Term.add_frees lhs' [])) [(x, T)];