anchor.diff:      in
       List.iter aux ps
   
  +let smt_pat_lid (r:Range.range) = Ident.set_lid_range C.smtpat_lid r
  +let smt_pat_or_lid (r:Range.range) = Ident.set_lid_range C.smtpatOr_lid r
  +
   (* TODO : Patterns should be checked that there are no incompatible type ascriptions *)
   (* and these type ascriptions should not be dropped !!!                              *)
   let rec desugar_data_pat
  
positive.code:       end
  
      | Construct (n, [(a, _)]) when n.str = "SMTPat" ->
          desugar_term_maybe_top top_level env ({top with tm = App ({top with tm = Var (lid_of_path ["Prims";"smt_pat"] top.range)}, a, Nothing)})
  
      | Construct (n, [(a, _)]) when n.str = "SMTPatT" ->
          Errors.log_issue top.range (Errors.Warning_SMTPatTDeprecated, "SMTPatT is deprecated; please just use SMTPat");
          desugar_term_maybe_top top_level env ({top with tm = App ({top with tm = Var (lid_of_path ["Prims";"smt_pat"] top.range)}, a, Nothing)})
  
      | Construct (n, [(a, _)]) when n.str = "SMTPatOr" ->
          desugar_term_maybe_top top_level env ({top with tm = App ({top with tm = Var (lid_of_path ["Prims";"smt_pat_or"] top.range)}, a, Nothing)})
  
      | Name {str="Type0"}  -> mk (Tm_type U_zero), noaqs
      | Name {str="Type"}   -> mk (Tm_type U_unknown), noaqs
  
negative.code:           | _other ->
              fail_lemma()
          in
          let head_and_attributes = fail_or env
            (Env.try_lookup_effect_name_and_attributes env)
            lemma in
          head_and_attributes, args
  
        | Name l when Env.is_effect_name env l ->
  