# HG changeset patch
# User boehmes
# Date 1254564616 -7200
# Node ID f8d1e16ec7580d7684035579c66b46b8eaaf3bb7
# Parent  a226f29d4bdcc0947a332906febaccde61238001# Parent  5e8cef567042fd5e8f3d3998b06ce93f17d7c364
merged

diff -r a226f29d4bdc -r f8d1e16ec758 Admin/isatest/isatest-makedist
--- a/Admin/isatest/isatest-makedist	Sat Oct 03 12:05:40 2009 +0200
+++ b/Admin/isatest/isatest-makedist	Sat Oct 03 12:10:16 2009 +0200
@@ -106,7 +106,7 @@
 sleep 15
 $SSH atbroy99 "$MAKEALL $HOME/settings/at64-poly"
 sleep 15
-$SSH macbroy2 "$MAKEALL $HOME/settings/mac-poly-M4; $MAKEALL $HOME/settings/mac-poly-M8; $MAKEALL $HOME/settings/mac-poly64-M4; $MAKEALL $HOME/settings/mac-poly64-M8"
+$SSH macbroy2 "$MAKEALL $HOME/settings/mac-poly64-M4; $MAKEALL $HOME/settings/mac-poly64-M8; $MAKEALL $HOME/settings/mac-poly-M4; $MAKEALL $HOME/settings/mac-poly-M8"
 sleep 15
 $SSH macbroy5 "$MAKEALL $HOME/settings/mac-poly"
 sleep 15
diff -r a226f29d4bdc -r f8d1e16ec758 Admin/isatest/settings/mac-poly64-M4
--- a/Admin/isatest/settings/mac-poly64-M4	Sat Oct 03 12:05:40 2009 +0200
+++ b/Admin/isatest/settings/mac-poly64-M4	Sat Oct 03 12:10:16 2009 +0200
@@ -4,7 +4,7 @@
   ML_SYSTEM="polyml-experimental"
   ML_PLATFORM="x86_64-darwin"
   ML_HOME="$POLYML_HOME/$ML_PLATFORM"
-  ML_OPTIONS="--mutable 5000 --immutable 2000"
+  ML_OPTIONS="--mutable 4000 --immutable 2000"
 
 
 ISABELLE_HOME_USER=~/isabelle-mac-poly64-M4
diff -r a226f29d4bdc -r f8d1e16ec758 Admin/isatest/settings/mac-poly64-M8
--- a/Admin/isatest/settings/mac-poly64-M8	Sat Oct 03 12:05:40 2009 +0200
+++ b/Admin/isatest/settings/mac-poly64-M8	Sat Oct 03 12:10:16 2009 +0200
@@ -4,7 +4,7 @@
   ML_SYSTEM="polyml-experimental"
   ML_PLATFORM="x86_64-darwin"
   ML_HOME="$POLYML_HOME/$ML_PLATFORM"
-  ML_OPTIONS="--mutable 5000 --immutable 2000"
+  ML_OPTIONS="--mutable 4000 --immutable 2000"
 
 
 ISABELLE_HOME_USER=~/isabelle-mac-poly64-M8
diff -r a226f29d4bdc -r f8d1e16ec758 src/HOL/Mirabelle/Tools/mirabelle_refute.ML
--- a/src/HOL/Mirabelle/Tools/mirabelle_refute.ML	Sat Oct 03 12:05:40 2009 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_refute.ML	Sat Oct 03 12:10:16 2009 +0200
@@ -9,11 +9,11 @@
 (* FIXME:
 fun refute_action args timeout {pre=st, ...} = 
   let
-    val subgoal = 0
+    val subgoal = 1
     val thy     = Proof.theory_of st
     val thm = goal_thm_of st
 
-    val refute = Refute.refute_subgoal thy args thm
+    val refute = Refute.refute_goal thy args thm
     val _ = TimeLimit.timeLimit timeout refute subgoal
   in
     val writ_log = Substring.full (the (Symtab.lookup tab "writeln"))
diff -r a226f29d4bdc -r f8d1e16ec758 src/HOL/Refute.thy
--- a/src/HOL/Refute.thy	Sat Oct 03 12:05:40 2009 +0200
+++ b/src/HOL/Refute.thy	Sat Oct 03 12:10:16 2009 +0200
@@ -1,5 +1,4 @@
 (*  Title:      HOL/Refute.thy
-    ID:         $Id$
     Author:     Tjark Weber
     Copyright   2003-2007
 
diff -r a226f29d4bdc -r f8d1e16ec758 src/HOL/Tools/ATP_Manager/atp_manager.ML
--- a/src/HOL/Tools/ATP_Manager/atp_manager.ML	Sat Oct 03 12:05:40 2009 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML	Sat Oct 03 12:10:16 2009 +0200
@@ -91,7 +91,6 @@
 );
 
 fun lookup_thread xs = AList.lookup Thread.equal xs;
-fun delete_thread xs = AList.delete Thread.equal xs;
 fun update_thread xs = AList.update Thread.equal xs;
 
 
@@ -117,7 +116,8 @@
 (* unregister thread *)
 
 fun unregister (success, message) thread = Synchronized.change state
-  (fn state as State {managing_thread, timeout_heap, oldest_heap, active, cancelling, messages, store} =>
+  (fn state as
+      State {managing_thread, timeout_heap, oldest_heap, active, cancelling, messages, store} =>
     (case lookup_thread active thread of
       SOME (birthtime, _, description) =>
         let
@@ -317,9 +317,11 @@
 fun print_provers thy = Pretty.writeln
   (Pretty.strs ("external provers:" :: sort_strings (Symtab.keys (Provers.get thy))));
 
-fun get_prover name thy = case Symtab.lookup (Provers.get thy) name of
-  NONE => NONE
-| SOME (prover, _) => SOME prover;
+fun get_prover name thy =
+  (case Symtab.lookup (Provers.get thy) name of
+    NONE => NONE
+  | SOME (prover, _) => SOME prover);
+
 
 (* start prover thread *)
 
diff -r a226f29d4bdc -r f8d1e16ec758 src/HOL/Tools/lin_arith.ML
--- a/src/HOL/Tools/lin_arith.ML	Sat Oct 03 12:05:40 2009 +0200
+++ b/src/HOL/Tools/lin_arith.ML	Sat Oct 03 12:10:16 2009 +0200
@@ -767,8 +767,6 @@
 
 structure Fast_Arith = Fast_Lin_Arith(structure LA_Logic = LA_Logic and LA_Data = LA_Data);
 
-val map_data = Fast_Arith.map_data;
-
 fun map_inj_thms f {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset, number_of} =
   {add_mono_thms = add_mono_thms, mult_mono_thms = mult_mono_thms, inj_thms = f inj_thms,
     lessD = lessD, neqE = neqE, simpset = simpset, number_of = number_of};
diff -r a226f29d4bdc -r f8d1e16ec758 src/HOL/Tools/old_primrec.ML
--- a/src/HOL/Tools/old_primrec.ML	Sat Oct 03 12:05:40 2009 +0200
+++ b/src/HOL/Tools/old_primrec.ML	Sat Oct 03 12:10:16 2009 +0200
@@ -318,31 +318,7 @@
 val add_primrec_unchecked = gen_primrec thy_note (thy_def true);
 val add_primrec_i = gen_primrec_i thy_note (thy_def false);
 val add_primrec_unchecked_i = gen_primrec_i thy_note (thy_def true);
-fun gen_primrec note def alt_name specs =
-  gen_primrec_i note def alt_name (map (fn ((name, t), atts) => ((name, atts), t)) specs);
 
 end;
 
-
-(* see primrec.ML (* outer syntax *)
-
-local structure P = OuterParse and K = OuterKeyword in
-
-val opt_unchecked_name =
-  Scan.optional (P.$$$ "(" |-- P.!!!
-    (((P.$$$ "unchecked" >> K true) -- Scan.optional P.name "" ||
-      P.name >> pair false) --| P.$$$ ")")) (false, "");
-
-val primrec_decl =
-  opt_unchecked_name -- Scan.repeat1 (SpecParse.opt_thm_name ":" -- P.prop);
-
-val _ =
-  OuterSyntax.command "primrec" "define primitive recursive functions on datatypes" K.thy_decl
-    (primrec_decl >> (fn ((unchecked, alt_name), eqns) =>
-      Toplevel.theory (snd o
-        (if unchecked then add_primrec_unchecked else add_primrec) alt_name
-          (map P.triple_swap eqns))));
-
-end;*)
-
 end;
diff -r a226f29d4bdc -r f8d1e16ec758 src/HOL/Tools/recdef.ML
--- a/src/HOL/Tools/recdef.ML	Sat Oct 03 12:05:40 2009 +0200
+++ b/src/HOL/Tools/recdef.ML	Sat Oct 03 12:10:16 2009 +0200
@@ -47,11 +47,6 @@
 fun map_congs f = map_hints (fn (simps, congs, wfs) => (simps, f congs, wfs));
 fun map_wfs f = map_hints (fn (simps, congs, wfs) => (simps, congs, f wfs));
 
-fun pretty_hints ({simps, congs, wfs}: hints) =
- [Pretty.big_list "recdef simp hints:" (map Display.pretty_thm_without_context simps),
-  Pretty.big_list "recdef cong hints:" (map Display.pretty_thm_without_context (map snd congs)),
-  Pretty.big_list "recdef wf hints:" (map Display.pretty_thm_without_context wfs)];
-
 
 (* congruence rules *)
 
diff -r a226f29d4bdc -r f8d1e16ec758 src/HOL/Tools/refute.ML
--- a/src/HOL/Tools/refute.ML	Sat Oct 03 12:05:40 2009 +0200
+++ b/src/HOL/Tools/refute.ML	Sat Oct 03 12:10:16 2009 +0200
@@ -51,9 +51,8 @@
   (* tries to find a model for a formula: *)
   val satisfy_term   : theory -> (string * string) list -> Term.term -> unit
   (* tries to find a model that refutes a formula: *)
-  val refute_term    : theory -> (string * string) list -> Term.term -> unit
-  val refute_subgoal :
-    theory -> (string * string) list -> Thm.thm -> int -> unit
+  val refute_term : theory -> (string * string) list -> term -> unit
+  val refute_goal : theory -> (string * string) list -> thm -> int -> unit
 
   val setup : theory -> theory
 
@@ -1355,16 +1354,11 @@
   end;
 
 (* ------------------------------------------------------------------------- *)
-(* refute_subgoal: calls 'refute_term' on a specific subgoal                 *)
-(* params        : list of '(name, value)' pairs used to override default    *)
-(*                 parameters                                                *)
-(* subgoal       : 0-based index specifying the subgoal number               *)
+(* refute_goal                                                               *)
 (* ------------------------------------------------------------------------- *)
 
-  (* theory -> (string * string) list -> Thm.thm -> int -> unit *)
-
-  fun refute_subgoal thy params thm subgoal =
-    refute_term thy params (List.nth (Thm.prems_of thm, subgoal));
+  fun refute_goal thy params st i =
+    refute_term thy params (Logic.get_goal (Thm.prop_of st) i);
 
 
 (* ------------------------------------------------------------------------- *)
diff -r a226f29d4bdc -r f8d1e16ec758 src/HOL/Tools/refute_isar.ML
--- a/src/HOL/Tools/refute_isar.ML	Sat Oct 03 12:05:40 2009 +0200
+++ b/src/HOL/Tools/refute_isar.ML	Sat Oct 03 12:10:16 2009 +0200
@@ -1,106 +1,52 @@
 (*  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, i) =>
+        Toplevel.keep (fn state =>
+          let
+            val thy = Toplevel.theory_of state;
+            val (_, st) = Proof.flat_goal (Toplevel.proof_of state);
+          in Refute.refute_goal thy parms st i 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                                                                 *)
-(* ------------------------------------------------------------------------- *)
+(* 'refute_params' command *)
 
-	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;
-
-	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 (x, y) => x ^ "=" ^ y) new_defaults));
+          val _ = writeln ("Default parameters for 'refute':\n" ^ output);
+        in thy' end)));
 
 end;
 
diff -r a226f29d4bdc -r f8d1e16ec758 src/Provers/clasimp.ML
--- a/src/Provers/clasimp.ML	Sat Oct 03 12:05:40 2009 +0200
+++ b/src/Provers/clasimp.ML	Sat Oct 03 12:10:16 2009 +0200
@@ -141,7 +141,6 @@
 
 val addXIs = modifier (ContextRules.intro_query NONE);
 val addXEs = modifier (ContextRules.elim_query NONE);
-val addXDs = modifier (ContextRules.dest_query NONE);
 val delXs = modifier ContextRules.rule_del;
 
 in
@@ -266,9 +265,6 @@
   HEADGOAL (Method.insert_tac (prems @ facts) THEN' tac (clasimpset_of ctxt)));
 
 
-fun clasimp_method tac =
-  Args.bang_facts --| Method.sections clasimp_modifiers >> (clasimp_meth tac);
-
 fun clasimp_method' tac =
   Args.bang_facts --| Method.sections clasimp_modifiers >> (clasimp_meth' tac);
 
diff -r a226f29d4bdc -r f8d1e16ec758 src/Provers/classical.ML
--- a/src/Provers/classical.ML	Sat Oct 03 12:05:40 2009 +0200
+++ b/src/Provers/classical.ML	Sat Oct 03 12:10:16 2009 +0200
@@ -696,13 +696,13 @@
 
 (*Backtracking is allowed among the various these unsafe ways of
   proving a subgoal.  *)
-fun inst0_step_tac (CS{safe0_netpair,safep_netpair,...}) =
-  assume_tac                      APPEND'
-  contr_tac                       APPEND'
+fun inst0_step_tac (CS {safe0_netpair, ...}) =
+  assume_tac APPEND'
+  contr_tac APPEND'
   biresolve_from_nets_tac safe0_netpair;
 
 (*These unsafe steps could generate more subgoals.*)
-fun instp_step_tac (CS{safep_netpair,...}) =
+fun instp_step_tac (CS {safep_netpair, ...}) =
   biresolve_from_nets_tac safep_netpair;
 
 (*These steps could instantiate variables and are therefore unsafe.*)
@@ -768,7 +768,7 @@
 (*Non-deterministic!  Could always expand the first unsafe connective.
   That's hard to implement and did not perform better in experiments, due to
   greater search depth required.*)
-fun dup_step_tac (cs as (CS{dup_netpair,...})) =
+fun dup_step_tac (CS {dup_netpair, ...}) =
   biresolve_from_nets_tac dup_netpair;
 
 (*Searching to depth m. A variant called nodup_depth_tac appears in clasimp.ML*)
@@ -910,7 +910,6 @@
 val introN = "intro";
 val elimN = "elim";
 val destN = "dest";
-val ruleN = "rule";
 
 val setup_attrs =
   Attrib.setup @{binding swapped} (Scan.succeed swapped)
diff -r a226f29d4bdc -r f8d1e16ec758 src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Sat Oct 03 12:05:40 2009 +0200
+++ b/src/Pure/Isar/isar_cmd.ML	Sat Oct 03 12:10:16 2009 +0200
@@ -450,14 +450,15 @@
   Pretty.string_of (Display.pretty_thms (Proof.context_of state) (Proof.get_thmss state args));
 
 fun string_of_prfs full state arg =
-  Pretty.string_of (case arg of
+  Pretty.string_of
+    (case arg of
       NONE =>
         let
-          val (ctxt, (_, thm)) = Proof.get_goal state;
+          val (ctxt, thm) = Proof.flat_goal state;
           val thy = ProofContext.theory_of ctxt;
           val prf = Thm.proof_of thm;
           val prop = Thm.full_prop_of thm;
-          val prf' = Proofterm.rewrite_proof_notypes ([], []) prf
+          val prf' = Proofterm.rewrite_proof_notypes ([], []) prf;
         in
           ProofSyntax.pretty_proof ctxt
             (if full then Reconstruct.reconstruct_proof thy prop prf' else prf')
diff -r a226f29d4bdc -r f8d1e16ec758 src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Sat Oct 03 12:05:40 2009 +0200
+++ b/src/Pure/Isar/proof.ML	Sat Oct 03 12:10:16 2009 +0200
@@ -431,9 +431,7 @@
 
 val refine = apply_text true;
 val refine_end = apply_text false;
-
-fun refine_insert [] = I
-  | refine_insert ths = Seq.hd o refine (Method.Basic (K (Method.insert ths)));
+fun refine_insert ths = Seq.hd o refine (Method.Basic (K (Method.insert ths)));
 
 end;
 
diff -r a226f29d4bdc -r f8d1e16ec758 src/Pure/Isar/specification.ML
--- a/src/Pure/Isar/specification.ML	Sat Oct 03 12:05:40 2009 +0200
+++ b/src/Pure/Isar/specification.ML	Sat Oct 03 12:10:16 2009 +0200
@@ -286,7 +286,7 @@
         val prems = Assumption.local_prems_of elems_ctxt ctxt;
         val stmt = Attrib.map_specs prep_att (map fst shows ~~ propp);
         val goal_ctxt = fold (fold (Variable.auto_fixes o fst)) propp elems_ctxt;
-      in ((prems, stmt, []), goal_ctxt) end
+      in ((prems, stmt, NONE), goal_ctxt) end
   | Element.Obtains obtains =>
       let
         val case_names = obtains |> map_index (fn (i, (b, _)) =>
@@ -327,7 +327,7 @@
           |> fold_map assume_case (obtains ~~ propp)
           |-> (fn ths => ProofContext.note_thmss Thm.assumptionK
                 [((Binding.name Obtain.thatN, []), [(ths, [])])] #> #2 #> pair ths);
-      in ((prems, stmt, facts), goal_ctxt) end);
+      in ((prems, stmt, SOME facts), goal_ctxt) end);
 
 structure TheoremHook = GenericDataFun
 (
@@ -372,7 +372,7 @@
       [((Binding.name AutoBind.assmsN, []), [(prems, [])])]
     |> snd
     |> Proof.theorem_i before_qed after_qed' (map snd stmt)
-    |> Proof.refine_insert facts
+    |> (case facts of NONE => I | SOME ths => Proof.refine_insert ths)
     |> Library.apply (map (fn (f, _) => f int) (rev (TheoremHook.get (Context.Proof goal_ctxt))))
   end;
 
diff -r a226f29d4bdc -r f8d1e16ec758 src/Pure/Tools/find_theorems.ML
--- a/src/Pure/Tools/find_theorems.ML	Sat Oct 03 12:05:40 2009 +0200
+++ b/src/Pure/Tools/find_theorems.ML	Sat Oct 03 12:10:16 2009 +0200
@@ -434,7 +434,7 @@
     let
       val proof_state = Toplevel.enter_proof_body state;
       val ctxt = Proof.context_of proof_state;
-      val opt_goal = try Proof.get_goal proof_state |> Option.map (#2 o #2);
+      val opt_goal = try Proof.flat_goal proof_state |> Option.map #2;
     in print_theorems ctxt opt_goal opt_lim rem_dups spec end);
 
 local
diff -r a226f29d4bdc -r f8d1e16ec758 src/Tools/auto_solve.ML
--- a/src/Tools/auto_solve.ML	Sat Oct 03 12:05:40 2009 +0200
+++ b/src/Tools/auto_solve.ML	Sat Oct 03 12:10:16 2009 +0200
@@ -16,7 +16,7 @@
   val limit : int Unsynchronized.ref
 end;
 
-structure AutoSolve : AUTO_SOLVE =
+structure Auto_Solve : AUTO_SOLVE =
 struct
 
 (* preferences *)
@@ -61,14 +61,14 @@
       end;
 
     fun seek_against_goal () =
-      (case try Proof.get_goal state of
+      (case try Proof.flat_goal state of
         NONE => NONE
-      | SOME (_, (_, goal)) =>
+      | SOME (_, st) =>
           let
-            val subgoals = Conjunction.dest_conjunctions (Thm.cprem_of goal 1);
+            val subgoals = Drule.strip_imp_prems (Thm.cprop_of st);
             val rs =
               if length subgoals = 1
-              then [(NONE, find goal)]
+              then [(NONE, find st)]
               else map (fn sg => (SOME sg, find (Goal.init sg))) subgoals;
             val results = filter_out (null o snd) rs;
           in if null results then NONE else SOME results end);
@@ -87,7 +87,7 @@
                   Pretty.markup Markup.hilite
                     (separate (Pretty.brk 0) (map prt_result results))])
         | _ => state)
-      end handle TimeLimit.TimeOut => (warning "AutoSolve: timeout."; state);
+      end handle TimeLimit.TimeOut => (warning "Auto solve: timeout"; state);
   in
     if int andalso ! auto andalso not (! Toplevel.quiet)
     then go ()
@@ -96,6 +96,6 @@
 
 end;
 
-val auto_solve = AutoSolve.auto;
-val auto_solve_time_limit = AutoSolve.auto_time_limit;
+val auto_solve = Auto_Solve.auto;
+val auto_solve_time_limit = Auto_Solve.auto_time_limit;
 
diff -r a226f29d4bdc -r f8d1e16ec758 src/Tools/induct.ML
--- a/src/Tools/induct.ML	Sat Oct 03 12:05:40 2009 +0200
+++ b/src/Tools/induct.ML	Sat Oct 03 12:10:16 2009 +0200
@@ -505,7 +505,6 @@
   let
     val thy = ProofContext.theory_of ctxt;
     val cert = Thm.cterm_of thy;
-    val certT = Thm.ctyp_of thy;
 
     val v = Free (x, T);
     fun spec_rule prfx (xs, body) =
@@ -579,7 +578,6 @@
 fun induct_tac ctxt def_insts arbitrary taking opt_rule facts =
   let
     val thy = ProofContext.theory_of ctxt;
-    val cert = Thm.cterm_of thy;
 
     val ((insts, defs), defs_ctxt) = fold_map add_defs def_insts ctxt |>> split_list;
     val atomized_defs = map (map (Conv.fconv_rule ObjectLogic.atomize)) defs;
@@ -652,7 +650,6 @@
 fun coinduct_tac ctxt inst taking opt_rule facts =
   let
     val thy = ProofContext.theory_of ctxt;
-    val cert = Thm.cterm_of thy;
 
     fun inst_rule r =
       if null inst then `RuleCases.get r
diff -r a226f29d4bdc -r f8d1e16ec758 src/Tools/induct_tacs.ML
--- a/src/Tools/induct_tacs.ML	Sat Oct 03 12:05:40 2009 +0200
+++ b/src/Tools/induct_tacs.ML	Sat Oct 03 12:10:16 2009 +0200
@@ -28,7 +28,7 @@
 
 fun gen_case_tac ctxt0 s opt_rule i st =
   let
-    val ((_, goal), ctxt) = Variable.focus_subgoal i st ctxt0;
+    val (_, ctxt) = Variable.focus_subgoal i st ctxt0;
     val rule =
       (case opt_rule of
         SOME rule => rule
diff -r a226f29d4bdc -r f8d1e16ec758 src/Tools/intuitionistic.ML
--- a/src/Tools/intuitionistic.ML	Sat Oct 03 12:05:40 2009 +0200
+++ b/src/Tools/intuitionistic.ML	Sat Oct 03 12:10:16 2009 +0200
@@ -69,7 +69,6 @@
 val introN = "intro";
 val elimN = "elim";
 val destN = "dest";
-val ruleN = "rule";
 
 fun modifier name kind kind' att =
   Args.$$$ name |-- (kind >> K NONE || kind' |-- OuterParse.nat --| Args.colon >> SOME)
diff -r a226f29d4bdc -r f8d1e16ec758 src/Tools/quickcheck.ML
--- a/src/Tools/quickcheck.ML	Sat Oct 03 12:05:40 2009 +0200
+++ b/src/Tools/quickcheck.ML	Sat Oct 03 12:10:16 2009 +0200
@@ -143,7 +143,7 @@
     val thy = Proof.theory_of state;
     fun strip (Const ("all", _) $ Abs (_, _, t)) = strip t
       | strip t = t;
-    val (_, (_, st)) = Proof.get_goal state;
+    val (_, st) = Proof.flat_goal state;
     val (gi, frees) = Logic.goal_params (prop_of st) i;
     val gi' = Logic.list_implies (assms, subst_bounds (frees, strip gi))
       |> monomorphic_term thy insts default_T