- procedural: bugfix in "Barendregt convention" test

[helm.git] / helm / software / components / acic_procedural / procedural2.ml

diff --git a/helm/software/components/acic_procedural/procedural2.ml b/helm/software/components/acic_procedural/procedural2.ml
index 9dcd20304dbab87e5ef3ffd2ca533472f1bbac74..f8007d3fc93b204c1fff97b5e0659d1d50245363 100644 (file)
--- a/helm/software/components/acic_procedural/procedural2.ml
+++ b/helm/software/components/acic_procedural/procedural2.ml
@@ -275,7 +275,7 @@ let mk_rewrite st dtext where qs tl direction t =
 
 let rec proc_lambda st what name v t =
    let name = match name with
-      | C.Anonymous -> H.mk_fresh_name st.context anonymous_premise
+      | C.Anonymous -> H.mk_fresh_name true st.context anonymous_premise
       | name        -> name
    in
    let entry = Some (name, C.Decl (H.cic v)) in