src/HOL/Tools/refute.ML
changeset 20548 8ef25fe585a8
parent 20544 893e7a9546ff
child 20854 f9cf9e62d11c
     1.1 --- a/src/HOL/Tools/refute.ML	Fri Sep 15 22:56:08 2006 +0200
     1.2 +++ b/src/HOL/Tools/refute.ML	Fri Sep 15 22:56:13 2006 +0200
     1.3 @@ -446,7 +446,7 @@
     1.4  				  SOME x => x
     1.5  				| NONE   => raise Type.TYPE_MATCH (* no match found - perhaps due to sort constraints *))
     1.6  		in
     1.7 -			map_term_types
     1.8 +			map_types
     1.9  				(map_type_tvar
    1.10  					(fn v =>
    1.11  						case Type.lookup (typeSubs, v) of
    1.12 @@ -461,7 +461,7 @@
    1.13  		(* term 't'                                                            *)
    1.14  		(* (Term.sort * Term.typ) Term.Vartab.table -> Term.term -> Term.term *)
    1.15  		fun monomorphic_term typeSubs t =
    1.16 -			map_term_types (map_type_tvar
    1.17 +			map_types (map_type_tvar
    1.18  				(fn v =>
    1.19  					case Type.lookup (typeSubs, v) of
    1.20  					  NONE =>