src/HOL/Real/Hyperreal/Filter.ML

 by (res_inst_tac [("x","U")] exI 1);
 by (Step_tac 1);
 by (Blast_tac 1);
 qed "FreeUltrafilter_ex";
 
-val FreeUltrafilter_Ex  = export FreeUltrafilter_ex;
+bind_thm ("FreeUltrafilter_Ex", export FreeUltrafilter_ex);
 
 Close_locale "UFT";