src/HOL/Hyperreal/fuf.ML

 
 fun get_fuf_hyps [] zs = zs
 |   get_fuf_hyps (x::xs) zs =
         case (concl_of x) of
         (_ $ (Const ("Not",_) $ (Const ("op :",_) $ _ $
-             Const ("StarType.FreeUltrafilterNat",_)))) =>  get_fuf_hyps xs
+             Const ("StarDef.FreeUltrafilterNat",_)))) =>  get_fuf_hyps xs
                                               ((x RS FreeUltrafilterNat_Compl_mem)::zs)
        |(_ $ (Const ("op :",_) $ _ $
-             Const ("StarType.FreeUltrafilterNat",_)))  =>  get_fuf_hyps xs (x::zs)
+             Const ("StarDef.FreeUltrafilterNat",_)))  =>  get_fuf_hyps xs (x::zs)
        | _ => get_fuf_hyps xs zs;
 
 fun inter_prems [] = raise FUFempty
 |   inter_prems [x] = x
 |   inter_prems (x::y::ys) =