src/HOL/Import/hol4rews.ML

 	    in
 		if not (defname mem used)
 		then F defname                 (* name_def *)
 		else if not (pdefname mem used)
 		then F pdefname                (* name_primdef *)
-		else F (variant used pdefname) (* last resort *)
+		else F (Name.variant used pdefname) (* last resort *)
 	    end
     end
 
 local
     fun handle_meta [x as Appl[Appl[Constant "_constrain", Constant "==", _],_,_]] = x