X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fassembly%2Ffreescale%2Fword16.ma;h=c47ff7d5136da098b57822ebb495df675b88ce4f;hb=0538bf9e109bbd963816e20254213a5df114ce84;hp=98d7703b636db370c1b85225f423986b4c3379d2;hpb=661ffd4d7c77fce52fb2f2d96f1737be424af3f1;p=helm.git

diff --git a/helm/software/matita/contribs/assembly/freescale/word16.ma b/helm/software/matita/contribs/assembly/freescale/word16.ma
index 98d7703b6..c47ff7d51 100644
--- a/helm/software/matita/contribs/assembly/freescale/word16.ma
+++ b/helm/software/matita/contribs/assembly/freescale/word16.ma
@@ -39,8 +39,7 @@ record word16 : Type ≝
 (* \langle \rangle *)
 notation "〈x:y〉" non associative with precedence 80
  for @{ 'mk_word16 $x $y }.
-interpretation "mk_word16" 'mk_word16 x y = 
- (cic:/matita/freescale/word16/word16.ind#xpointer(1/1/1) x y).
+interpretation "mk_word16" 'mk_word16 x y = (mk_word16 x y).
 
 (* operatore = *)
 definition eq_w16 ≝ λw1,w2.(eq_b8 (w16h w1) (w16h w2)) ⊗ (eq_b8 (w16l w1) (w16l w2)).