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