anchor.diff:  let cbox () = () //close_box()
   let ``break`` () = () //print_break 0 0
     
  -let small t = match t with | TmVar (_, _, _) -> true | _ -> false
  +let small t =
  +    match t with
  +    | TmVar (_, _, _) -> true
  +    | _ -> false
     
   let rec printty_Type outer tyT =
  -  match tyT with | tyT -> printty_ArrowType outer tyT
  +  match tyT with
  +  | tyT -> printty_ArrowType outer tyT
   
   and printty_ArrowType outer tyT =
  -  match tyT with
  -  | TyArr (tyT1, tyT2) ->
  -      (obox0 ();
  -       printty_AType false tyT1;
  -       if outer then pr " " else ();
  -       pr "->";
  -       if outer then print_space () else ``break`` ();
  -       printty_ArrowType outer tyT2;
  -       cbox ())
  -  | tyT -> printty_AType outer tyT
  +    match tyT with
  +    | TyArr (tyT1, tyT2) ->
  +        obox0 ()
  +        printty_AType false tyT1
  +        if outer then pr " " else ()
  +        pr "->"
  +        if outer then print_space () else ``break`` ()
  +        printty_ArrowType outer tyT2
  +        cbox ()
  +    | tyT ->
  +        printty_AType outer tyT
   
   and printty_AType outer tyT =
  -  match tyT with
  -  | TyTop -> pr "Top"
  -  | TyBot -> pr "Bot"
  -  | tyT -> (pr "("; printty_Type outer tyT; pr ")")
  +    match tyT with
  +    | TyTop -> pr "Top"
  +    | TyBot -> pr "Bot"
  +    | tyT ->
  +        pr "("
  +        printty_Type outer tyT
  +        pr ")"
     
   let printty tyT = printty_Type true tyT
     
   let rec printtm_Term outer ctx t =
  -  match t with
  -  | TmAbs (fi, x, tyT1, t2) ->
  -      let (ctx', x') = pickfreshname ctx x
  -      in
  -        (obox ();
  -         pr "lambda ";
  -         pr x';
  -         pr ":";
  -         printty_Type false tyT1;
  -         pr ".";
  -         if (small t2) && (not outer) then ``break`` () else print_space ();
  -         printtm_Term outer ctx' t2;
  -         cbox ())
  -  | t -> printtm_AppTerm outer ctx t
  +    match t with
  +    | TmAbs (fi, x, tyT1, t2) ->
  +        let ctx', x' = pickfreshname ctx x
  +        obox ()
  +        pr "lambda "
  +        pr x'
  +        pr ":"
  +        printty_Type false tyT1
  +        pr "."
  +        if small t2 && not outer then ``break`` () else print_space ()
  +        printtm_Term outer ctx' t2
  +        cbox ()
  +    | t ->
  +        printtm_AppTerm outer ctx t
   
   and printtm_AppTerm outer ctx t =
  -  match t with
  -  | TmApp (fi, t1, t2) ->
  -      (obox0 ();
  -       printtm_AppTerm false ctx t1;
  -       print_space ();
  -       printtm_ATerm false ctx t2;
  -       cbox ())
  -  | t -> printtm_ATerm outer ctx t
  +    match t with
  +    | TmApp (fi, t1, t2) ->
  +        obox0 ()
  +        printtm_AppTerm false ctx t1
  +        print_space ()
  +        printtm_ATerm false ctx t2
  +        cbox ()
  +    | t ->
  +        printtm_ATerm outer ctx t
   
   and printtm_ATerm outer ctx t =
     match t with
     | TmVar (fi, x, n) ->
  -      if (ctxlength ctx) = n
  -      then pr (index2name fi ctx x)
  +      if (ctxlength ctx) = n then
  +        pr (index2name fi ctx x)
         else
           pr
             ("[bad index: " ^
  
positive.code: let printtm ctx t = printtm_Term true ctx t
    
  let prbinding ctx b =
    match b with | NameBind -> () | VarBind tyT -> (pr ": "; printty tyT)
    
  
negative.code: 
  (* ---------------------------------------------------------------------- *)
  (* Datatypes *)
  type ty =
      | TyTop
      | TyBot
      | TyArr of ty * ty
  
  type term =
      | TmVar of info * int * int
      | TmAbs of info * string * ty * term
      | TmApp of info * term * term
  
  type binding =
      | NameBind
      | VarBind of ty
  
  type context = (string * binding) list
  
  type command =
      | Eval of info * term
      | Bind of info * string * binding
  
  (* ---------------------------------------------------------------------- *)
  (* Context management *)
  let emptycontext = []
    
  let ctxlength ctx =
      List.length ctx
    
  let addbinding ctx x bind =
      (x, bind) :: ctx
    
  let addname ctx x =
      addbinding ctx x NameBind
    
  let rec isnamebound ctx x =
      match ctx with
      | [] ->
          false
      | (y, _) :: rest ->
          if y = x then true
          else isnamebound rest x
    
  let rec pickfreshname ctx x =
      if isnamebound ctx x then
          pickfreshname ctx (x + "'")
      else
          ((x, NameBind) :: ctx), x
    
  let index2name fi ctx x =
      try let xn, _ = List.nth ctx x
          xn
      with
      | Failure _ ->
          let msg = sprintf "Variable lookup failure: offset: %d, ctx size: %d"
          error fi (msg x (List.length ctx))
    
  let rec name2index fi ctx x =
      match ctx with
      | [] ->
          error fi ("Identifier " ^ (x ^ " is unbound"))
      | (y, _) :: rest ->
          if y = x then 0
          else 1 + (name2index fi rest x)
    
  (* ---------------------------------------------------------------------- *)
  (* Shifting *)
  let tmmap onvar c t =
      let rec walk c t =
          match t with
          | TmVar (fi, x, n) ->
              onvar fi c x n
          | TmAbs (fi, x, tyT1, t2) ->
              TmAbs (fi, x, tyT1, walk (c + 1) t2)
          | TmApp (fi, t1, t2) ->
              TmApp (fi, walk c t1, walk c t2)
      walk c t
    
  let termShiftAbove d c t =
      (c, t)
      ||> tmmap (fun fi c x n ->
          if x >= c then TmVar (fi, x + d, n + d)
          else TmVar (fi, x, n + d))
    
  let termShift d t =
      termShiftAbove d 0 t
    
  (* ---------------------------------------------------------------------- *)
  (* Substitution *)
  let termSubst j s t =
      (j, t)
      ||> tmmap (fun fi j x n ->
          if x = j then termShift j s
          else TmVar (fi, x, n))
    
  let termSubstTop s t =
      termShift -1 (termSubst 0 (termShift 1 s) t)
    
  (* ---------------------------------------------------------------------- *)
  (* Context management (continued) *)
  let rec getbinding fi ctx i =
      try let _, bind = List.nth ctx i
          bind
      with Failure _ ->
          let msg = sprintf "Variable lookup failure: offset: %d, ctx size: %d"
          error fi (msg i (List.length ctx))
    
  let getTypeFromContext fi ctx i =
      match getbinding fi ctx i with
      | VarBind tyT -> tyT
      | _ ->
          error fi ("getTypeFromContext: Wrong kind of binding for variable " + (index2name fi ctx i))
    
  (* ---------------------------------------------------------------------- *)
  (* Extracting file info *)
  let tmInfo t =
      match t with
      | TmVar (fi, _, _) -> fi
      | TmAbs (fi, _, _, _) -> fi
      | TmApp (fi, _, _) -> fi
    
  (* ---------------------------------------------------------------------- *)
  (* Printing *)
  