anchor.diff:  
     let env0 = env in
   
  -  let env1, tys, datas =  //AR: env1 contains the opened universe names if any
  -    if List.length univs = 0 then env, tys, datas
  -    else
  -      let subst, univs = SS.univ_var_opening univs in
  -      let tys = List.map (fun se ->
  -        let sigel = match se.sigel with
  -          | Sig_inductive_typ (lid, _, bs, t, l1, l2) ->
  -            Sig_inductive_typ (lid, univs, SS.subst_binders subst bs, SS.subst (SS.shift_subst (List.length bs) subst) t, l1, l2)
  -          | _ -> failwith "Impossible, can't happen"
  -        in
  -        { se with sigel = sigel }) tys
  -      in
  -      let datas = List.map (fun se ->
  -        let sigel = match se.sigel with
  -          | Sig_datacon (lid, _, t, lid_t, x, l) ->
  -            Sig_datacon (lid, univs, SS.subst subst t, lid_t, x, l)
  -          | _ -> failwith "Impossible, can't happen"
  -        in
  -        { se with sigel = sigel }) datas
  -      in
  -      Env.push_univ_vars env univs, tys, datas
  -  in
  -
     (* Check each tycon *)
     let env, tcs, g = List.fold_right (fun tc (env, all_tcs, g)  ->
       let env, tc, tc_u, guard = tc_tycon env tc in
       let g' = Rel.universe_inequality S.U_zero tc_u in
       if Env.debug env Options.Low then BU.print1 "Checked inductive: %s\n" (Print.sigelt_to_string tc);
       env, (tc, tc_u)::all_tcs, Env.conj_guard g (Env.conj_guard guard g')
  -  ) tys (env1, [], Env.trivial_guard)
  +  ) tys (env, [], Env.trivial_guard)
     in
   
     (* Check each datacon *)
  
positive.code:   then raise_error (Errors.Fatal_NonInductiveInMutuallyDefinedType, ("Mutually defined type contains a non-inductive element")) (Env.get_range env);
  
    //AR: adding this code for the second phase
    //    univs need not be empty, so open all along
    let univs =
      if List.length tys = 0 then []
      else
  
negative.code:     let tc_universe_vars = List.map snd tcs in
      let g = {g with univ_ineqs=tc_universe_vars, snd (g.univ_ineqs)} in
  
      if Env.debug env0 <| Options.Other "GenUniverses"
      then BU.print1 "@@@@@@Guard before (possible) generalization: %s\n" (Rel.guard_to_string env g);
  
      Rel.force_trivial_guard env0 g;
      if List.length univs = 0 then generalize_and_inst_within env0 g tcs datas
      else (List.map fst tcs), datas
    in
  
  