src/HOL/Tools/res_axioms.ML

 	val thm'' = if (is_elimR thm') then (cnf_elim thm')  else cnf_rule thm'
     in
 	rm_redundant_cls thm''
     end;
 
-fun meta_cnf_axiom thm = map (zero_var_indexes o make_meta_clause) (cnf_axiom thm);
+fun meta_cnf_axiom thm = 
+    map (zero_var_indexes o Meson.make_meta_clause) (cnf_axiom thm);
 
 
 (* changed: with one extra case added *)
 fun univ_vars_of_aux (Const ("Hilbert_Choice.Eps",_) $ Abs(_,_,body)) vars = univ_vars_of_aux body vars
   | univ_vars_of_aux (Const ("Ex",_) $ Abs(_,_,body)) vars = univ_vars_of_aux body vars (* EX x. body *)