--- a/src/Pure/Isar/constdefs.ML Tue Mar 03 18:31:59 2009 +0100
+++ b/src/Pure/Isar/constdefs.ML Tue Mar 03 18:32:01 2009 +0100
@@ -36,7 +36,7 @@
val prop = prep_prop var_ctxt raw_prop;
val (c, T) = #1 (LocalDefs.cert_def thy_ctxt (Logic.strip_imp_concl prop));
val _ =
- (case Option.map Binding.base_name d of
+ (case Option.map Binding.name_of d of
NONE => ()
| SOME c' =>
if c <> c' then
@@ -44,7 +44,7 @@
else ());
val def = Term.subst_atomic [(Free (c, T), Const (Sign.full_bname thy c, T))] prop;
- val name = Thm.def_name_optional c (Binding.base_name raw_name);
+ val name = Thm.def_name_optional c (Binding.name_of raw_name);
val atts = map (prep_att thy) raw_atts;
val thy' =