# HG changeset patch
# User wenzelm
# Date 1254509492 -7200
# Node ID 7da2447fadf20333aed0d079c350abc98038598d
# Parent  7dd4b559e177589257d7d67569593d4ce0b78ad4
misc tuning and simplification;

diff -r 7dd4b559e177 -r 7da2447fadf2 src/HOL/Tools/refute_isar.ML
--- a/src/HOL/Tools/refute_isar.ML	Fri Oct 02 20:10:25 2009 +0200
+++ b/src/HOL/Tools/refute_isar.ML	Fri Oct 02 20:51:32 2009 +0200
@@ -1,106 +1,53 @@
 (*  Title:      HOL/Tools/refute_isar.ML
-    ID:         $Id$
     Author:     Tjark Weber
     Copyright   2003-2007
 
-Adds the 'refute' and 'refute_params' commands to Isabelle/Isar's outer
-syntax.
+Outer syntax commands 'refute' and 'refute_params'.
 *)
 
-structure RefuteIsar: sig end =
+structure Refute_Isar: sig end =
 struct
 
-(* ------------------------------------------------------------------------- *)
-(* common functions for argument parsing/scanning                            *)
-(* ------------------------------------------------------------------------- *)
-
-(* ------------------------------------------------------------------------- *)
-(* both 'refute' and 'refute_params' take an optional list of arguments of   *)
-(* the form [name1=value1, name2=value2, ...]                                *)
-(* ------------------------------------------------------------------------- *)
+(* argument parsing *)
 
-	val scan_parm = OuterParse.name -- (OuterParse.$$$ "=" |-- OuterParse.name);
+(*optional list of arguments of the form [name1=value1, name2=value2, ...]*)
 
-	val scan_parms = Scan.option
-		(OuterParse.$$$ "[" |-- (OuterParse.list scan_parm) --| OuterParse.$$$ "]");
-
-(* ------------------------------------------------------------------------- *)
-(* set up the 'refute' command                                               *)
-(* ------------------------------------------------------------------------- *)
+val scan_parm = OuterParse.name -- (OuterParse.$$$ "=" |-- OuterParse.name);
 
-(* ------------------------------------------------------------------------- *)
-(* 'refute' takes an optional list of parameters, followed by an optional    *)
-(* subgoal number                                                            *)
-(* ------------------------------------------------------------------------- *)
-
-	val refute_scan_args = scan_parms -- (Scan.option OuterParse.nat);
-
-(* ------------------------------------------------------------------------- *)
-(* the 'refute' command is mapped to 'Refute.refute_subgoal'                 *)
-(* ------------------------------------------------------------------------- *)
+val scan_parms = Scan.optional
+  (OuterParse.$$$ "[" |-- OuterParse.list scan_parm --| OuterParse.$$$ "]") [];
 
-	fun refute_trans args =
-		Toplevel.keep (fn state =>
-			let
-				val (parms_opt, subgoal_opt) = args
-				val parms   = Option.getOpt (parms_opt, [])
-				val subgoal = Option.getOpt (subgoal_opt, 1) - 1
-				val thy     = Toplevel.theory_of state
-				val thm     = (snd o snd) (Proof.get_goal (Toplevel.proof_of state))
-			in
-				Refute.refute_subgoal thy parms thm subgoal
-			end);
 
-	fun refute_parser tokens = (refute_scan_args tokens) |>> refute_trans;
+(* 'refute' command *)
 
-	val _ = OuterSyntax.improper_command "refute"
-		"try to find a model that refutes a given subgoal"
-		OuterKeyword.diag refute_parser;
-
-(* ------------------------------------------------------------------------- *)
-(* set up the 'refute_params' command                                        *)
-(* ------------------------------------------------------------------------- *)
+val _ =
+  OuterSyntax.improper_command "refute"
+    "try to find a model that refutes a given subgoal" OuterKeyword.diag
+    (scan_parms -- Scan.optional OuterParse.nat 1 >> (fn (parms, subgoal) =>
+      Toplevel.keep (fn state =>
+        let
+          val thy = Toplevel.theory_of state
+          val st = (snd o snd) (Proof.get_goal (Toplevel.proof_of state))
+        in
+          Refute.refute_subgoal thy parms st (subgoal - 1)
+        end)));
 
-(* ------------------------------------------------------------------------- *)
-(* 'refute_params' takes an optional list of parameters                      *)
-(* ------------------------------------------------------------------------- *)
-
-	val refute_params_scan_args = scan_parms;
-
-(* ------------------------------------------------------------------------- *)
-(* the 'refute_params' command is mapped to (multiple calls of)              *)
-(* 'Refute.set_default_param'; then the (new) default parameters are         *)
-(* displayed                                                                 *)
-(* ------------------------------------------------------------------------- *)
 
-	fun refute_params_trans args =
-		let
-			fun add_params thy [] =
-				thy
-			  | add_params thy (p::ps) =
-				add_params (Refute.set_default_param p thy) ps
-		in
-			Toplevel.theory (fn thy =>
-				let
-					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
-							cat_lines (map (fn (name, value) => name ^ "=" ^ value)
-								new_default_params)
-				in
-					writeln ("Default parameters for 'refute':\n" ^ output);
-					thy'
-				end)
-		end;
+(* 'refute_params' command *)
 
-	fun refute_params_parser tokens =
-		(refute_params_scan_args tokens) |>> refute_params_trans;
-
-	val _ = OuterSyntax.command "refute_params"
-		"show/store default parameters for the 'refute' command"
-		OuterKeyword.thy_decl refute_params_parser;
+val _ =
+  OuterSyntax.command "refute_params"
+    "show/store default parameters for the 'refute' command" OuterKeyword.thy_decl
+    (scan_parms >> (fn parms =>
+      Toplevel.theory (fn thy =>
+        let
+          val thy' = fold Refute.set_default_param parms thy
+          val output =
+            (case Refute.get_default_params thy' of
+              [] => "none"
+            | new_defaults => cat_lines (map (fn (name, value) => name ^ "=" ^ value) new_defaults))
+          val _ = writeln ("Default parameters for 'refute':\n" ^ output);
+        in thy' end)))
 
 end;