# HG changeset patch
# User webertj
# Date 1168453164 -3600
# Node ID 7c81de75d2c327f6146fa34a4fc54299e460597d
# Parent  4cb2fe751952419e1c0c06d192833e3f67184ac8
tuned

diff -r 4cb2fe751952 -r 7c81de75d2c3 src/HOL/Tools/refute.ML
--- a/src/HOL/Tools/refute.ML	Wed Jan 10 19:18:29 2007 +0100
+++ b/src/HOL/Tools/refute.ML	Wed Jan 10 19:19:24 2007 +0100
@@ -1233,7 +1233,7 @@
 	(* theory -> (string * string) list -> Thm.thm -> int -> unit *)
 
 	fun refute_subgoal thy params thm subgoal =
-		refute_term thy params (List.nth (prems_of thm, subgoal));
+		refute_term thy params (List.nth (Thm.prems_of thm, subgoal));
 
 
 (* ------------------------------------------------------------------------- *)