diff -r 4eaae533efc3 -r 4a10338c2535 Nominal/Parser.thy
--- a/Nominal/Parser.thy	Wed Mar 10 12:48:55 2010 +0100
+++ b/Nominal/Parser.thy	Wed Mar 10 16:50:42 2010 +0100
@@ -155,7 +155,7 @@
 *}
 
 ML {*
-fun prep_bn dt_names dts eqs lthy = 
+fun prep_bn dt_names dts eqs = 
 let
   fun aux eq = 
   let
@@ -241,7 +241,7 @@
   
   val raw_binds = rawify_binds dts_env cnstrs_env bn_fun_full_env binds 
 
-  val raw_bns = prep_bn dt_full_names' raw_dts (map snd raw_bn_eqs) lthy
+  val raw_bns = prep_bn dt_full_names' raw_dts (map snd raw_bn_eqs)
 
   val _ = tracing (cat_lines (map PolyML.makestring raw_bns)) 
 in