# HG changeset patch
# User wenzelm
# Date 1283440336 -7200
# Node ID 4006f5c3f421f2eba4e05fc9e032f1da3a0f55fe
# Parent  cdff476ba39e0b0f84cf8f34d3c421ae580f47c4
just one refute.ML;

diff -r cdff476ba39e -r 4006f5c3f421 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Thu Sep 02 16:45:21 2010 +0200
+++ b/src/HOL/IsaMakefile	Thu Sep 02 17:12:16 2010 +0200
@@ -209,7 +209,6 @@
   Tools/primrec.ML \
   Tools/prop_logic.ML \
   Tools/refute.ML \
-  Tools/refute_isar.ML \
   Tools/rewrite_hol_proof.ML \
   Tools/sat_funcs.ML \
   Tools/sat_solver.ML \
diff -r cdff476ba39e -r 4006f5c3f421 src/HOL/Refute.thy
--- a/src/HOL/Refute.thy	Thu Sep 02 16:45:21 2010 +0200
+++ b/src/HOL/Refute.thy	Thu Sep 02 17:12:16 2010 +0200
@@ -9,9 +9,7 @@
 
 theory Refute
 imports Hilbert_Choice List
-uses
-  "Tools/refute.ML"
-  "Tools/refute_isar.ML"
+uses "Tools/refute.ML"
 begin
 
 setup Refute.setup
@@ -92,16 +90,14 @@
 (* ------------------------------------------------------------------------- *)
 (* FILES                                                                     *)
 (*                                                                           *)
-(* HOL/Tools/prop_logic.ML    Propositional logic                            *)
-(* HOL/Tools/sat_solver.ML    SAT solvers                                    *)
-(* HOL/Tools/refute.ML        Translation HOL -> propositional logic and     *)
-(*                            Boolean assignment -> HOL model                *)
-(* HOL/Tools/refute_isar.ML   Adds 'refute'/'refute_params' to Isabelle's    *)
-(*                            syntax                                         *)
-(* HOL/Refute.thy             This file: loads the ML files, basic setup,    *)
-(*                            documentation                                  *)
-(* HOL/SAT.thy                Sets default parameters                        *)
-(* HOL/ex/RefuteExamples.thy  Examples                                       *)
+(* HOL/Tools/prop_logic.ML     Propositional logic                           *)
+(* HOL/Tools/sat_solver.ML     SAT solvers                                   *)
+(* HOL/Tools/refute.ML         Translation HOL -> propositional logic and    *)
+(*                             Boolean assignment -> HOL model               *)
+(* HOL/Refute.thy              This file: loads the ML files, basic setup,   *)
+(*                             documentation                                 *)
+(* HOL/SAT.thy                 Sets default parameters                       *)
+(* HOL/ex/Refute_Examples.thy  Examples                                      *)
 (* ------------------------------------------------------------------------- *)
 \end{verbatim}
 *}
diff -r cdff476ba39e -r 4006f5c3f421 src/HOL/Tools/refute.ML
--- a/src/HOL/Tools/refute.ML	Thu Sep 02 16:45:21 2010 +0200
+++ b/src/HOL/Tools/refute.ML	Thu Sep 02 17:12:16 2010 +0200
@@ -3257,5 +3257,47 @@
    add_printer "stlc" stlc_printer #>
    add_printer "IDT"  IDT_printer;
 
+
+
+(** outer syntax commands 'refute' and 'refute_params' **)
+
+(* argument parsing *)
+
+(*optional list of arguments of the form [name1=value1, name2=value2, ...]*)
+
+val scan_parm = Parse.name -- (Scan.optional (Parse.$$$ "=" |-- Parse.name) "true")
+val scan_parms = Scan.optional (Parse.$$$ "[" |-- Parse.list scan_parm --| Parse.$$$ "]") [];
+
+
+(* 'refute' command *)
+
+val _ =
+  Outer_Syntax.improper_command "refute"
+    "try to find a model that refutes a given subgoal" Keyword.diag
+    (scan_parms -- Scan.optional Parse.nat 1 >>
+      (fn (parms, i) =>
+        Toplevel.keep (fn state =>
+          let
+            val ctxt = Toplevel.context_of state;
+            val {goal = st, ...} = Proof.raw_goal (Toplevel.proof_of state);
+          in refute_goal ctxt parms st i end)));
+
+
+(* 'refute_params' command *)
+
+val _ =
+  Outer_Syntax.command "refute_params"
+    "show/store default parameters for the 'refute' command" Keyword.thy_decl
+    (scan_parms >> (fn parms =>
+      Toplevel.theory (fn thy =>
+        let
+          val thy' = fold set_default_param parms thy;
+          val output =
+            (case get_default_params thy' of
+              [] => "none"
+            | new_defaults => cat_lines (map (fn (x, y) => x ^ "=" ^ y) new_defaults));
+          val _ = writeln ("Default parameters for 'refute':\n" ^ output);
+        in thy' end)));
+
 end;
 
diff -r cdff476ba39e -r 4006f5c3f421 src/HOL/Tools/refute_isar.ML
--- a/src/HOL/Tools/refute_isar.ML	Thu Sep 02 16:45:21 2010 +0200
+++ b/src/HOL/Tools/refute_isar.ML	Thu Sep 02 17:12:16 2010 +0200
@@ -2,49 +2,6 @@
     Author:     Tjark Weber
     Copyright   2003-2007
 
-Outer syntax commands 'refute' and 'refute_params'.
-*)
-
-structure Refute_Isar: sig end =
-struct
-
-(* argument parsing *)
-
-(*optional list of arguments of the form [name1=value1, name2=value2, ...]*)
-
-val scan_parm = Parse.name -- (Scan.optional (Parse.$$$ "=" |-- Parse.name) "true")
-val scan_parms = Scan.optional (Parse.$$$ "[" |-- Parse.list scan_parm --| Parse.$$$ "]") [];
-
-
-(* 'refute' command *)
-
-val _ =
-  Outer_Syntax.improper_command "refute"
-    "try to find a model that refutes a given subgoal" Keyword.diag
-    (scan_parms -- Scan.optional Parse.nat 1 >>
-      (fn (parms, i) =>
-        Toplevel.keep (fn state =>
-          let
-            val ctxt = Toplevel.context_of state;
-            val {goal = st, ...} = Proof.raw_goal (Toplevel.proof_of state);
-          in Refute.refute_goal ctxt parms st i end)));
-
-
-(* 'refute_params' command *)
-
-val _ =
-  Outer_Syntax.command "refute_params"
-    "show/store default parameters for the 'refute' command" Keyword.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 (x, y) => x ^ "=" ^ y) new_defaults));
-          val _ = writeln ("Default parameters for 'refute':\n" ^ output);
-        in thy' end)));
 
 end;