X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_transformations%2Fsequent2pres.ml;h=b7de8499a1404df236de4459ae606626ad73f7e2;hb=97c2d258a5c524eb5c4b85208899d80751a2c82f;hp=bac0f1509da11e12665461c105c54e8261b9c8d9;hpb=08ecc780b3b0a4cac7ed72cf68c310e4eeffa2c1;p=helm.git

diff --git a/helm/ocaml/cic_transformations/sequent2pres.ml b/helm/ocaml/cic_transformations/sequent2pres.ml
index bac0f1509..b7de8499a 100644
--- a/helm/ocaml/cic_transformations/sequent2pres.ml
+++ b/helm/ocaml/cic_transformations/sequent2pres.ml
@@ -76,7 +76,7 @@ let sequent2pres term2pres (_,_,context,ty) =
                 (match def_name with
                    None -> "_"
                  | Some n -> n)) ;
-                 Box.b_text [] ":=" ;
+                 Box.b_text [] (Utf8Macro.unicode_of_tex "\\def") ;
                 term2pres bo] in
          aux (r::accum) tl
       | _::_ -> assert false in