src/HOL/Tools/refute.ML

 			  | find_typeSubs (t1 $ t2)          = (case find_typeSubs t1 of SOME x => SOME x | NONE => find_typeSubs t2)
 			val typeSubs = (case find_typeSubs t of
 				  SOME x => x
 				| NONE   => raise Type.TYPE_MATCH (* no match found - perhaps due to sort constraints *))
 		in
-			map_term_types
+			map_types
 				(map_type_tvar
 					(fn v =>
 						case Type.lookup (typeSubs, v) of
 						  NONE =>
 							(* schematic type variable not instantiated *)

 		end
 		(* applies a type substitution 'typeSubs' for all type variables in a  *)
 		(* term 't'                                                            *)
 		(* (Term.sort * Term.typ) Term.Vartab.table -> Term.term -> Term.term *)
 		fun monomorphic_term typeSubs t =
-			map_term_types (map_type_tvar
+			map_types (map_type_tvar
 				(fn v =>
 					case Type.lookup (typeSubs, v) of
 					  NONE =>
 						(* schematic type variable not instantiated *)
 						error ""