diff -r 28e71a685c84 -r 2b47822868e4 src/HOL/Tools/inductive_realizer.ML
--- a/src/HOL/Tools/inductive_realizer.ML	Thu Jun 09 15:38:49 2011 +0200
+++ b/src/HOL/Tools/inductive_realizer.ML	Thu Jun 09 16:34:49 2011 +0200
@@ -36,7 +36,7 @@
 
 fun strip_all' used names (Const ("all", _) $ Abs (s, T, t)) =
       let val (s', names') = (case names of
-          [] => (Name.variant used s, [])
+          [] => (singleton (Name.variant_list used) s, [])
         | name :: names' => (name, names'))
       in strip_all' (s'::used) names' (subst_bound (Free (s', T), t)) end
   | strip_all' used names ((t as Const ("==>", _) $ P) $ Q) =
@@ -246,7 +246,7 @@
     handle Datatype_Aux.Datatype_Empty name' =>
       let
         val name = Long_Name.base_name name';
-        val dname = Name.variant used "Dummy";
+        val dname = singleton (Name.variant_list used) "Dummy";
       in
         thy
         |> add_dummies f (map (add_dummy (Binding.name name) (Binding.name dname)) dts) (dname :: used)