Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
tuned
authorwebertj
Wed, 10 Jan 2007 19:19:24 +0100
changeset 22055 7c81de75d2c3
parent 22054 4cb2fe751952
child 22056 858016d00449
tuned
src/HOL/Tools/refute.ML file | annotate | diff | comparison | revisions 
--- 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));
 
 
 (* ------------------------------------------------------------------------- *)
isabelle