minor code refactoring
authorwebertj
Fri Nov 12 20:55:04 2004 +0100 (2004-11-12)
changeset 15280e0e9bf44afad
parent 15279 95cc0d447916
child 15281 bd4611956c7b
minor code refactoring
src/HOL/Tools/refute.ML
     1.1 --- a/src/HOL/Tools/refute.ML	Fri Nov 12 16:26:19 2004 +0100
     1.2 +++ b/src/HOL/Tools/refute.ML	Fri Nov 12 20:55:04 2004 +0100
     1.3 @@ -440,6 +440,18 @@
     1.4  							typ))
     1.5  					t
     1.6  		end
     1.7 +		(* applies a type substitution 'typeSubs' for all type variables in a  *)
     1.8 +		(* term 't'                                                            *)
     1.9 +		(* Term.typ Term.Vartab.table -> Term.term -> Term.term *)
    1.10 +		fun monomorphic_term typeSubs t =
    1.11 +			map_term_types (map_type_tvar
    1.12 +				(fn (v,_) =>
    1.13 +					case Vartab.lookup (typeSubs, v) of
    1.14 +					  None =>
    1.15 +						(* schematic type variable not instantiated *)
    1.16 +						raise ERROR
    1.17 +					| Some typ =>
    1.18 +						typ)) t
    1.19  		(* Term.term list * Term.typ -> Term.term list *)
    1.20  		fun collect_type_axioms (axs, T) =
    1.21  			case T of
    1.22 @@ -472,18 +484,8 @@
    1.23  								let
    1.24  									val T''      = (domain_type o domain_type) T'
    1.25  									val typeSubs = Type.typ_match (Sign.tsig_of (sign_of thy)) (Vartab.empty, (T'', T))
    1.26 -									val unvar_ax = map_term_types
    1.27 -										(map_type_tvar
    1.28 -											(fn (v,_) =>
    1.29 -												case Vartab.lookup (typeSubs, v) of
    1.30 -												  None =>
    1.31 -													(* schematic type variable not instantiated *)
    1.32 -													raise ERROR
    1.33 -												| Some typ =>
    1.34 -													typ))
    1.35 -										ax
    1.36  								in
    1.37 -									Some (axname, unvar_ax)
    1.38 +									Some (axname, monomorphic_term typeSubs ax)
    1.39  								end
    1.40  							| None =>
    1.41  								get_typedefn axms
    1.42 @@ -572,18 +574,8 @@
    1.43  							if s=s' then
    1.44  								let
    1.45  									val typeSubs = Type.typ_match (Sign.tsig_of (sign_of thy)) (Vartab.empty, (T', T))
    1.46 -									val unvar_ax = map_term_types
    1.47 -										(map_type_tvar
    1.48 -											(fn (v,_) =>
    1.49 -												case Vartab.lookup (typeSubs, v) of
    1.50 -												  None =>
    1.51 -													(* schematic type variable not instantiated *)
    1.52 -													raise ERROR
    1.53 -												| Some typ =>
    1.54 -													typ))
    1.55 -										ax
    1.56  								in
    1.57 -									Some (axname, unvar_ax)
    1.58 +									Some (axname, monomorphic_term typeSubs ax)
    1.59  								end
    1.60  							else
    1.61  								get_defn axms