--- a/src/HOL/BNF/Tools/bnf_def.ML Sun Sep 23 08:24:19 2012 +0200
+++ b/src/HOL/BNF/Tools/bnf_def.ML Sun Sep 23 14:52:53 2012 +0200
@@ -692,9 +692,9 @@
||>> 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)*)