--- a/Nominal/nominal_induct.ML	Mon May 09 04:49:58 2011 +0100
+++ b/Nominal/nominal_induct.ML	Tue May 10 07:47:06 2011 +0100
@@ -95,7 +95,7 @@
     val finish_rule =
       split_all_tuples
       #> rename_params_rule true
-        (map (Name.clean o ProofContext.revert_skolem defs_ctxt o fst) avoiding);
+        (map (Name.clean o Variable.revert_fixed defs_ctxt o fst) avoiding);
 
     fun rule_cases ctxt r =
       let val r' = if simp then Induct.simplified_rule ctxt r else r