changeset 35845 | e5980f0ad025 |
parent 35691 | d9c9b81b16a8 |
child 36610 | bafd82950e24 |
--- a/src/Pure/Isar/constdefs.ML Sat Mar 20 02:23:41 2010 +0100 +++ b/src/Pure/Isar/constdefs.ML Sat Mar 20 17:33:11 2010 +0100 @@ -56,7 +56,7 @@ |> Sign.add_consts_i [(b, T, mx)] |> PureThy.add_defs false [((name, def), atts)] |-> (fn [thm] => (* FIXME thm vs. atts !? *) - Spec_Rules.add_global Spec_Rules.Equational ([Logic.varify head], [thm]) #> + Spec_Rules.add_global Spec_Rules.Equational ([Logic.varify_global head], [thm]) #> Code.add_default_eqn thm); in ((c, T), thy') end;