# HG changeset patch
# User webertj
# Date 1126016979 -7200
# Node ID e95f7141ba2f3f88d5cd8eee58dad8cb5062eb8c
# Parent  c63e5220ed77bdf6ca743edc8c36044df2037392
unnecessary parentheses removed

diff -r c63e5220ed77 -r e95f7141ba2f src/HOL/Tools/refute_isar.ML
--- 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)