1.1 --- a/src/HOL/Import/hol4rews.ML	Thu Jun 09 15:38:49 2011 +0200
     1.2 +++ b/src/HOL/Import/hol4rews.ML	Thu Jun 09 16:34:49 2011 +0200
     1.3 @@ -605,7 +605,7 @@
     1.4                  then F defname                 (* name_def *)
     1.5                  else if not (member (op =) used pdefname)
     1.6                  then F pdefname                (* name_primdef *)
     1.7 -                else F (Name.variant used pdefname) (* last resort *)
     1.8 +                else F (singleton (Name.variant_list used) pdefname) (* last resort *)
     1.9              end
    1.10      end
    1.11