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