src/Pure/primitive_defs.ML
changeset 30364 577edc39b501
parent 30280 eb98b49ef835
child 33385 fb2358edcfb6
     1.1 --- a/src/Pure/primitive_defs.ML	Sun Mar 08 17:19:15 2009 +0100
     1.2 +++ b/src/Pure/primitive_defs.ML	Sun Mar 08 17:26:14 2009 +0100
     1.3 @@ -81,7 +81,7 @@
     1.4  fun mk_defpair (lhs, rhs) =
     1.5    (case Term.head_of lhs of
     1.6      Const (name, _) =>
     1.7 -      (NameSpace.base_name name ^ "_def", Logic.mk_equals (lhs, rhs))
     1.8 +      (Long_Name.base_name name ^ "_def", Logic.mk_equals (lhs, rhs))
     1.9    | _ => raise TERM ("Malformed definition: head of lhs not a constant", [lhs, rhs]));
    1.10  
    1.11  end;