src/Pure/Isar/specification.ML
changeset 24624 b8383b1bbae3
parent 24557 57e2a5fbde86
child 24676 63eaef3207e1
     1.1 --- a/src/Pure/Isar/specification.ML	Tue Sep 18 07:36:14 2007 +0200
     1.2 +++ b/src/Pure/Isar/specification.ML	Tue Sep 18 07:36:15 2007 +0200
     1.3 @@ -131,7 +131,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, Code.add_func_attr false :: atts), [prove lthy2 th]);
     1.8 +          ((name, Code.add_default_func_attr :: 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)];