X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Focaml%2Facic_content%2FcicNotationUtil.ml;h=8e487ed11ed293374f4737a39bbc0e975b0165ff;hb=ee8a9f2a9f75814be05fa9f7aafefb3e42692a2a;hp=0aa6b48b32a4936aecfd83d934158b0208079194;hpb=9a0e4f3be9f70662f18d2d3b6dd60ae79fba565b;p=helm.git

diff --git a/helm/ocaml/acic_content/cicNotationUtil.ml b/helm/ocaml/acic_content/cicNotationUtil.ml
index 0aa6b48b3..8e487ed11 100644
--- a/helm/ocaml/acic_content/cicNotationUtil.ml
+++ b/helm/ocaml/acic_content/cicNotationUtil.ml
@@ -23,6 +23,8 @@
  * http://helm.cs.unibo.it/
  *)
 
+(* $Id$ *)
+
 module Ast = CicNotationPt
 
 let visit_ast ?(special_k = fun _ -> assert false) k =
@@ -364,6 +366,7 @@ let freshen_obj obj =
   let index = ref 0 in
   let freshen_term = freshen_term ~index in
   let freshen_name_ty = List.map (fun (n, t) -> (n, freshen_term t)) in
+  let freshen_name_ty_b = List.map (fun (n, t, b) -> (n, freshen_term t, b)) in
   match obj with
   | CicNotationPt.Inductive (params, indtypes) ->
       let indtypes =
@@ -379,7 +382,7 @@ let freshen_obj obj =
       CicNotationPt.Theorem (flav, n, freshen_term t, ty_opt)
   | CicNotationPt.Record (params, n, ty, fields) ->
       CicNotationPt.Record (freshen_name_ty params, n, freshen_term ty,
-        freshen_name_ty fields)
+        freshen_name_ty_b fields)
 
 let freshen_term = freshen_term ?index:None