src/HOL/BNF/Tools/bnf_def.ML

       ||>> mk_Frees "e1" (map2 (curry (op -->)) B1Ts ranTs')
       ||>> mk_Frees "e2" (map2 (curry (op -->)) B2Ts ranTs'')
       ||>> mk_Frees "p1" (map2 (curry (op -->)) domTs B1Ts)
       ||>> mk_Frees "p2" (map2 (curry (op -->)) domTs B2Ts)
       ||>> mk_Frees "b" As'
-      ||>> mk_Frees' "R" setRTs
-      ||>> mk_Frees "R" setRTs
-      ||>> mk_Frees "S" setRTsBsCs
+      ||>> mk_Frees' "S" setRTs
+      ||>> mk_Frees "S" setRTs
+      ||>> mk_Frees "T" setRTsBsCs
       ||>> mk_Frees' "Q" QTs;
 
     (*Gr (in R1 .. Rn) (map fst .. fst)^-1 O Gr (in R1 .. Rn) (map snd .. snd)*)
     val O_Gr =
       let