--- a/Nominal/Nominal2.thy	Mon Jul 20 11:21:59 2015 +0100
+++ b/Nominal/Nominal2.thy	Sat Mar 19 21:06:48 2016 +0000
@@ -178,7 +178,7 @@
   val raw_induct_thms = #inducts (hd dtinfos)
   val raw_exhaust_thms = map #exhaust dtinfos
   val raw_size_trms = map HOLogic.size_const raw_tys
-  val raw_size_thms = these (Option.map ((fn ths => drop (length ths div 2) ths) o fst o snd)
+  val raw_size_thms = these (Option.map ((fn ths => drop (length ths div 2) ths) o #2 o #2)
     (BNF_LFP_Size.size_of lthy1 (hd raw_full_dt_names')))
 
   val raw_result = RawDtInfo