anchor.diff:                                  build_branch_guard sub_term ei) |> List.flatten in
                            discriminate scrutinee_tm f @ sub_term_guards
                   | _ -> [] //a non-pattern sub-term: must be from a dot pattern
  -          in 
  +          in
   
             (* 6 (b) *)
             let build_and_check_branch_guard scrutinee_tm pat =
  
positive.code:             | None -> branch_guard
              | Some w -> Util.mk_conj branch_guard w in
  
            branch_guard 
    in
  
    let guard = Rel.conj_guard g_when g_branch in
  
negative.code:           S.mk t None e.pos in
        universe_of_type e <| N.normalize [N.Beta; N.UnfoldUntil Delta_constant] env t
  
  let universe_of env e =
     match universe_or_type_of env e with
     | Inl t ->
       raise (Error(Util.format2 "Expected a term of type 'Type'; got %s : %s"
                          (Print.term_to_string e)
                          (Print.term_to_string t),
                    Env.get_range env))
     | Inr u -> u