# HG changeset patch
# User wenzelm
# Date 1184681682 -7200
# Node ID ad6ad61332fa558d2792e687ab512d5f61c07ad7
# Parent  3fe991a1f80502edd7a09d452408c52c574a8ed9
avoid redundant variables in patterns (which made Alice vomit);

diff -r 3fe991a1f805 -r ad6ad61332fa src/Pure/ProofGeneral/pgip_markup.ML
--- a/src/Pure/ProofGeneral/pgip_markup.ML	Tue Jul 17 16:06:13 2007 +0200
+++ b/src/Pure/ProofGeneral/pgip_markup.ML	Tue Jul 17 16:14:42 2007 +0200
@@ -81,7 +81,7 @@
                                  opt_attr "metavarid" (#metavarid vs),
                     [])
 
-         | Closeblock vs =>
+         | Closeblock _ =>
            XML.Elem("closeblock", [], [])
 
          | Opentheory vs  =>
@@ -156,8 +156,8 @@
 
    fun unparse_elt docelt =
    case docelt of
-       Openblock vs => ""
-     | Closeblock vs => ""
+       Openblock _ => ""
+     | Closeblock _ => ""
      | Opentheory vs => #text vs
      | Theoryitem vs => #text vs
      | Closetheory vs => #text vs
diff -r 3fe991a1f805 -r ad6ad61332fa src/Pure/ProofGeneral/pgip_output.ML
--- a/src/Pure/ProofGeneral/pgip_output.ML	Tue Jul 17 16:06:13 2007 +0200
+++ b/src/Pure/ProofGeneral/pgip_output.ML	Tue Jul 17 16:14:42 2007 +0200
@@ -350,7 +350,7 @@
                  content)
     end
 
-fun ready (Ready vs) = XML.Elem("ready",[],[])
+fun ready (Ready _) = XML.Elem("ready",[],[])
 
 
 fun output pgipoutput = case pgipoutput of
diff -r 3fe991a1f805 -r ad6ad61332fa src/Pure/ProofGeneral/proof_general_pgip.ML
--- a/src/Pure/ProofGeneral/proof_general_pgip.ML	Tue Jul 17 16:06:13 2007 +0200
+++ b/src/Pure/ProofGeneral/proof_general_pgip.ML	Tue Jul 17 16:14:42 2007 +0200
@@ -513,17 +513,17 @@
 (* Responses to each of the PGIP input commands.
    These are programmed uniformly for extensibility. *)
 
-fun askpgip (Askpgip vs) =
+fun askpgip (Askpgip _) =
     (issue_pgip
          (Usespgip { version = PgipIsabelle.isabelle_pgip_version_supported,
                      pgipelems = PgipIsabelle.accepted_inputs });
      send_pgip_config())
 
-fun askpgml (Askpgml vs) =
+fun askpgml (Askpgml _) =
     issue_pgip
         (Usespgml { version = PgipIsabelle.isabelle_pgml_version_supported })
 
-fun askprefs (Askprefs vs) =
+fun askprefs (Askprefs _) =
     let
         fun preference_of {name, descr, default, pgiptype, get, set } =
             { name = name, descr = SOME descr, default = SOME default,
@@ -535,7 +535,7 @@
                  (!preferences)
     end
 
-fun askconfig (Askconfig vs) = () (* TODO: add config response *)
+fun askconfig (Askconfig _) = () (* TODO: add config response *)
 
 local
     fun lookuppref pref =
@@ -563,9 +563,9 @@
     end
 end
 
-fun proverinit vs = restart ()
+fun proverinit _ = restart ()
 
-fun proverexit vs = isarcmd "quit"
+fun proverexit _ = isarcmd "quit"
 
 fun set_proverflag_quiet b = 
     isarcmd (if b then "disable_pr" else "enable_pr")
@@ -608,9 +608,9 @@
         isarcmd ("undos_proof " ^ Int.toString times)
     end
 
-fun redostep vs = isarcmd "redo"
+fun redostep _ = isarcmd "redo"
 
-fun abortgoal vs = isarcmd "kill" (* was: ProofGeneral.kill_proof *)
+fun abortgoal _ = isarcmd "kill" (* was: ProofGeneral.kill_proof *)
 
 
 (*** PGIP identifier tables ***)
@@ -791,7 +791,7 @@
 
 fun get_currently_open_file () = ! currently_open_file;
 
-fun askguise vs =
+fun askguise _ =
     (* The "guise" is the PGIP abstraction of the prover's state.
        The <informguise> message is merely used for consistency checking. *)
     let
@@ -830,9 +830,9 @@
                                   errs = map PgipOutput.output errs })
     end
 
-fun showproofstate vs = isarcmd "pr"
+fun showproofstate _ = isarcmd "pr"
 
-fun showctxt vs = isarcmd "print_context"
+fun showctxt _ = isarcmd "print_context"
 
 fun searchtheorems (Searchtheorems vs) =
     let
@@ -864,13 +864,13 @@
         isarcmd text
     end
 
-fun undoitem vs =
+fun undoitem _ =
     isarcmd "undo"
 
-fun redoitem vs =
+fun redoitem _ =
     isarcmd "redo"
 
-fun aborttheory vs =
+fun aborttheory _ =
     isarcmd "kill"  (* was: "init_toplevel" *)
 
 fun retracttheory (Retracttheory vs) =
@@ -930,7 +930,7 @@
                    currently_open_file := SOME url)
   end
 
-fun closefile vs =
+fun closefile _ =
     case !currently_open_file of
         SOME f => (proper_inform_file_processed f (Isar.state());
                    priority ("Finished working in file: " ^ PgipTypes.string_of_pgipurl f);
@@ -951,7 +951,7 @@
         use_thy_or_ml_file (File.platform_path url)
     end
 
-fun abortfile vs =
+fun abortfile _ =
     case !currently_open_file of
         SOME f => (isarcmd "init_toplevel";
                    priority ("Aborted working in file: " ^
@@ -984,7 +984,7 @@
   end
 
 exception PGIP_QUIT;
-fun quitpgip vs = raise PGIP_QUIT
+fun quitpgip _ = raise PGIP_QUIT
 
 fun process_input inp = case inp
  of Pgip.Askpgip _          => askpgip inp