diff -r 7bc38b93a1fc -r 9ae285ce814e Nominal/Nominal2.thy
--- a/Nominal/Nominal2.thy	Sun Apr 06 13:07:24 2014 +0100
+++ b/Nominal/Nominal2.thy	Fri May 16 08:38:23 2014 +0100
@@ -178,9 +178,8 @@
   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 = Size.size_thms (Proof_Context.theory_of lthy1) (hd raw_full_dt_names')
-    |> `(fn thms => (length thms) div 2)
-    |> uncurry drop
+  val raw_size_thms = these (Option.map ((fn ths => drop (length ths div 2) ths) o fst o snd)
+    (BNF_LFP_Size.lookup_size lthy1 (hd raw_full_dt_names')))
 
   val raw_result = RawDtInfo 
     {raw_dt_names = raw_full_dt_names',