src/Pure/Isar/constdefs.ML
changeset 32662 2faf1148c062
parent 30763 6976521b4263
child 33389 bb3a5fa94a91
     1.1 --- a/src/Pure/Isar/constdefs.ML	Wed Sep 23 16:20:12 2009 +0200
     1.2 +++ b/src/Pure/Isar/constdefs.ML	Wed Sep 23 16:20:12 2009 +0200
     1.3 @@ -52,7 +52,7 @@
     1.4        thy
     1.5        |> Sign.add_consts_i [(b, T, mx)]
     1.6        |> PureThy.add_defs false [((name, def), atts)]
     1.7 -      |-> (fn [thm] => Code.add_default_eqn thm);
     1.8 +      |-> (fn [thm] => Code.add_default_eqn thm #> Context.theory_map (Predicate_Compile_Preproc_Const_Defs.add_thm 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 =