
diff -r 84a13d1e2511 -r 0c9ef14e9ba4 Nominal/NewParser.thy
--- 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




