anchor.diff:   
   let lident2mlsymbol (l:lident) : mlsymbol = l.ident.idText
   
  -let extractCtor (c:context) (ctor: inductiveConstructor):  (mlsymbol * list<mlty>) =
  +let bindersOfFuntype (t:typ) : list<binder> = 
  +match ((Util.compress_typ t).n) with
  +| Typ_fun (lb,_) -> lb
  +| _ -> [] 
  +    //printfn "%A\n" (ctor.ctype);
  +    //failwith "was expecting a function type"
  +
  +let rec zipUnequal (la : list<'a>) (lb : list<'b>) : list<('a * 'b)> =
  +match  (la, lb) with
  +| (ha::ta, hb::tb) -> ((ha,hb)::(zipUnequal ta tb))
  +| _ -> []
  +
  +let extractCtor (c:context) (tyBinders : list<binder>) (ctor: inductiveConstructor):  (mlsymbol * list<mlty>) =
      if (0< List.length ctor.cargs)
      then (failwith "cargs is unexpectedly non-empty. This is a design-flaw, please report.")
      else 
  -        (let mlt = extractTyp c ctor.ctype in
  +        (let lb= bindersOfFuntype ctor.ctype in 
  +        let lp = zipUnequal tyBinders lb in
  +        assert (List.length tyBinders = List.length lp);
  +        let newC = extendContextWithRepAsTyVars (List.map (fun (x,y) -> (fst x, fst y)) lp) c in
  +        let mlt = extractTyp newC ctor.ctype in
               // fprint1 "extracting the type of constructor %s\n" (lident2mlsymbol ctor.cname);
               //fprint1 "%s\n" (typ_to_string ctor.ctype);
               // printfn "%A\n" (ctor.ctype);
  
positive.code: 
  
  let btvar2mlident (btv: btvar) : mlident =  (prependTick (convIdent btv.v.ppname)) 
  
  let extendContextAsTyvar (availableInML : bool) (b : either<btvar,bvvar>) (c:context): context = 
  match b with
  
negative.code:     let ind = parseFirstInductiveType s in
      //let k = lookup_typ_lid c ind.tyName in
      let identsPP = List.map binderPPnames ind.tyBinders in
      let newContext = c in // (extendContext c (mfst ind.tyBinders)) in
      let nIndices = numIndices ind.k.n ind.tyName.ident.idText in
      let tyDecBody = MLTD_DType (List.map (extractCtor newContext ind.tyBinders) ind.constructors) in
            Some (MLS_Ty [(lident2mlsymbol ind.tyName, List.append (List.map (fun x -> prependTick (convIdent x)) identsPP) (dummyIndexIdents nIndices)  , Some tyDecBody)])
  | _ -> None
  
  