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/NewParser.thy
changeset 1963 0c9ef14e9ba4
parent 1960 47e2e91705f3
child 1964 209ee65b2395 
--- a/Nominal/NewParser.thy	Tue Apr 27 22:21:16 2010 +0200
+++ b/Nominal/NewParser.thy	Tue Apr 27 22:45:50 2010 +0200
@@ -277,7 +277,7 @@
   val thy = Local_Theory.exit_global lthy2;
   val lthy3 = Theory_Target.init NONE thy;
 
-  val (_, lthy4) = define_fv dtinfo bn_funs_decls raw_bclauses lthy3;
+  val (_, lthy4) = define_raw_fv dtinfo bn_funs_decls raw_bclauses lthy3;
 in
   ((raw_dt_names, raw_bn_funs_loc, raw_bn_eqs_loc, raw_bclauses, raw_bns), lthy4)
 end
nominal2