src/Pure/primitive_defs.ML

--- a/src/Pure/primitive_defs.ML	Thu Mar 05 11:58:53 2009 +0100
+++ b/src/Pure/primitive_defs.ML	Thu Mar 05 12:08:00 2009 +0100
@@ -81,7 +81,7 @@
 fun mk_defpair (lhs, rhs) =
   (case Term.head_of lhs of
     Const (name, _) =>
-      (NameSpace.base name ^ "_def", Logic.mk_equals (lhs, rhs))
+      (NameSpace.base_name name ^ "_def", Logic.mk_equals (lhs, rhs))
   | _ => raise TERM ("Malformed definition: head of lhs not a constant", [lhs, rhs]));
 
 end;