# HG changeset patch
# User webertj
# Date 1100289304 -3600
# Node ID e0e9bf44afad0440ac59e81f5c4a8b336b27a603
# Parent  95cc0d4479163b9921befae09db8cafed9a985ac
minor code refactoring

diff -r 95cc0d447916 -r e0e9bf44afad src/HOL/Tools/refute.ML
--- a/src/HOL/Tools/refute.ML	Fri Nov 12 16:26:19 2004 +0100
+++ b/src/HOL/Tools/refute.ML	Fri Nov 12 20:55:04 2004 +0100
@@ -440,6 +440,18 @@
 							typ))
 					t
 		end
+		(* applies a type substitution 'typeSubs' for all type variables in a  *)
+		(* term 't'                                                            *)
+		(* Term.typ Term.Vartab.table -> Term.term -> Term.term *)
+		fun monomorphic_term typeSubs t =
+			map_term_types (map_type_tvar
+				(fn (v,_) =>
+					case Vartab.lookup (typeSubs, v) of
+					  None =>
+						(* schematic type variable not instantiated *)
+						raise ERROR
+					| Some typ =>
+						typ)) t
 		(* Term.term list * Term.typ -> Term.term list *)
 		fun collect_type_axioms (axs, T) =
 			case T of
@@ -472,18 +484,8 @@
 								let
 									val T''      = (domain_type o domain_type) T'
 									val typeSubs = Type.typ_match (Sign.tsig_of (sign_of thy)) (Vartab.empty, (T'', T))
-									val unvar_ax = map_term_types
-										(map_type_tvar
-											(fn (v,_) =>
-												case Vartab.lookup (typeSubs, v) of
-												  None =>
-													(* schematic type variable not instantiated *)
-													raise ERROR
-												| Some typ =>
-													typ))
-										ax
 								in
-									Some (axname, unvar_ax)
+									Some (axname, monomorphic_term typeSubs ax)
 								end
 							| None =>
 								get_typedefn axms
@@ -572,18 +574,8 @@
 							if s=s' then
 								let
 									val typeSubs = Type.typ_match (Sign.tsig_of (sign_of thy)) (Vartab.empty, (T', T))
-									val unvar_ax = map_term_types
-										(map_type_tvar
-											(fn (v,_) =>
-												case Vartab.lookup (typeSubs, v) of
-												  None =>
-													(* schematic type variable not instantiated *)
-													raise ERROR
-												| Some typ =>
-													typ))
-										ax
 								in
-									Some (axname, unvar_ax)
+									Some (axname, monomorphic_term typeSubs ax)
 								end
 							else
 								get_defn axms