src/Pure/Isar/specification.ML
changeset 24219 e558fe311376
parent 22923 6384c43da028
child 24452 93b113c5ac33
     1.1 --- a/src/Pure/Isar/specification.ML	Fri Aug 10 17:04:24 2007 +0200
     1.2 +++ b/src/Pure/Isar/specification.ML	Fri Aug 10 17:04:34 2007 +0200
     1.3 @@ -130,7 +130,7 @@
     1.4        |> LocalTheory.def Thm.definitionK ((x, mx), ((name ^ "_raw", []), rhs));
     1.5      val ((b, [th']), lthy3) = lthy2
     1.6        |> LocalTheory.note Thm.definitionK
     1.7 -          ((name, CodegenData.add_func_attr false :: atts), [prove lthy2 th]);
     1.8 +          ((name, Code.add_func_attr false :: atts), [prove lthy2 th]);
     1.9  
    1.10      val lhs' = Morphism.term (LocalTheory.target_morphism lthy3) lhs;
    1.11      val _ = print_consts lthy3 (member (op =) (Term.add_frees lhs' [])) [(x, T)];