src/HOL/Tools/refute_isar.ML
changeset 15570 8d8c70b41bab
parent 14454 8a8330bef1f8
child 17057 0934ac31985f
     1.1 --- a/src/HOL/Tools/refute_isar.ML	Thu Mar 03 09:22:35 2005 +0100
     1.2 +++ b/src/HOL/Tools/refute_isar.ML	Thu Mar 03 12:43:01 2005 +0100
     1.3 @@ -48,7 +48,7 @@
     1.4  					val thy              = (Toplevel.theory_of state)
     1.5  					val thm              = ((snd o snd) (Proof.get_goal (Toplevel.proof_of state)))
     1.6  				in
     1.7 -					Refute.refute_subgoal thy (if_none parms []) thm ((if_none subgoal 1)-1)
     1.8 +					Refute.refute_subgoal thy (getOpt (parms, [])) thm ((getOpt (subgoal, 1))-1)
     1.9  				end)
    1.10  			);
    1.11  
    1.12 @@ -79,7 +79,7 @@
    1.13  		in
    1.14  			Toplevel.theory (fn thy =>
    1.15  				let
    1.16 -					val thy'               = add_params (thy, (if_none args []))
    1.17 +					val thy'               = add_params (thy, (getOpt (args, [])))
    1.18  					val new_default_params = Refute.get_default_params thy'
    1.19  					val output             = if new_default_params=[] then "none" else (space_implode "\n" (map (fn (name,value) => name ^ "=" ^ value) new_default_params))
    1.20  				in