1.1 --- a/src/Pure/Isar/constdefs.ML	Fri Sep 26 09:09:53 2008 +0200
     1.2 +++ b/src/Pure/Isar/constdefs.ML	Fri Sep 26 09:10:02 2008 +0200
     1.3 @@ -54,7 +54,7 @@
     1.4        thy
     1.5        |> Sign.add_consts_i [(c, T, mx)]
     1.6        |> PureThy.add_defs false [((name, def), atts)]
     1.7 -      |-> (fn [thm] => Code.add_default_func thm);
     1.8 +      |-> (fn [thm] => Code.add_default_eqn thm);
     1.9    in ((c, T), thy') end;
    1.10  
    1.11  fun gen_constdefs prep_vars prep_prop prep_att (raw_structs, specs) thy =