diff -r f89773ab0685 -r a2f70c09e77d Nominal/NewParser.thy
--- a/Nominal/NewParser.thy	Mon May 17 16:29:33 2010 +0200
+++ b/Nominal/NewParser.thy	Mon May 17 16:25:45 2010 +0100
@@ -406,12 +406,11 @@
   val lthy3 = Theory_Target.init NONE thy;
   val raw_bn_funs = map (fn (f, _, _) => f) raw_bns;
 
-  val ((fv, fvbn), fv_def, lthy3a) = 
+  val (fv, fvbn, fv_def, lthy3a) = 
     if get_STEPS lthy2 > 3 
-    then define_raw_fv descr sorts raw_bns raw_bclauses lthy3
+    then define_raw_fvs descr sorts raw_bns raw_bclauses lthy3
     else raise TEST lthy3
   
-
   (* definition of raw alphas *)
   val (((alpha_ts, alpha_intros), (alpha_cases, alpha_induct)), lthy4) =
     if get_STEPS lthy > 4