src/HOL/Tools/refute_isar.ML
changeset 17273 e95f7141ba2f
parent 17057 0934ac31985f
child 22092 ab3dfcef6489
--- a/src/HOL/Tools/refute_isar.ML	Tue Sep 06 16:24:53 2005 +0200
+++ b/src/HOL/Tools/refute_isar.ML	Tue Sep 06 16:29:39 2005 +0200
@@ -1,7 +1,7 @@
 (*  Title:      HOL/Tools/refute_isar.ML
     ID:         $Id$
     Author:     Tjark Weber
-    Copyright   2003-2004
+    Copyright   2003-2005
 
 Adds the 'refute' and 'refute_params' commands to Isabelle/Isar's outer
 syntax.
@@ -45,8 +45,8 @@
 			(fn state =>
 				(let
 					val (parms, subgoal) = args
-					val thy              = (Toplevel.theory_of state)
-					val thm              = ((snd o snd) (Proof.get_goal (Toplevel.proof_of state)))
+					val thy              = Toplevel.theory_of state
+					val thm              = (snd o snd) (Proof.get_goal (Toplevel.proof_of state))
 				in
 					Refute.refute_subgoal thy (getOpt (parms, [])) thm ((getOpt (subgoal, 1))-1)
 				end)