Mercurial Mercurial > hg > nominal2 / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Nominal/Parser.thy
changeset 1403 4a10338c2535
parent 1392 baa67b07f436
child 1404 56ce001cdb87 
--- 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
nominal2