merged

--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Tue Oct 26 14:06:22 2010 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Tue Oct 26 15:00:57 2010 +0200
@@ -316,11 +316,10 @@
 
 fun get_prover ctxt args =
   let
-    val thy = ProofContext.theory_of ctxt
     fun default_prover_name () =
       hd (#provers (Sledgehammer_Isar.default_params ctxt []))
       handle Empty => error "No ATP available."
-    fun get_prover name = (name, Sledgehammer.get_prover thy false name)
+    fun get_prover name = (name, Sledgehammer.get_prover ctxt false name)
   in
     (case AList.lookup (op =) args proverK of
       SOME name => get_prover name

--- a/src/HOL/Tools/Function/partial_function.ML	Tue Oct 26 14:06:22 2010 +0200
+++ b/src/HOL/Tools/Function/partial_function.ML	Tue Oct 26 15:00:57 2010 +0200
@@ -228,7 +228,7 @@
 val mode = Parse.$$$ "(" |-- Parse.xname --| Parse.$$$ ")";
 
 val _ = Outer_Syntax.local_theory
-  "partial_function" "define partial function" Keyword.thy_goal
+  "partial_function" "define partial function" Keyword.thy_decl
   ((mode -- (Parse.fixes -- (Parse.where_ |-- Parse_Spec.spec)))
      >> (fn (mode, (fixes, spec)) => add_partial_function_cmd mode fixes spec));
 

--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Tue Oct 26 14:06:22 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Tue Oct 26 15:00:57 2010 +0200
@@ -63,7 +63,7 @@
   val kill_provers : unit -> unit
   val running_provers : unit -> unit
   val messages : int option -> unit
-  val get_prover : theory -> bool -> string -> prover
+  val get_prover : Proof.context -> bool -> string -> prover
   val run_sledgehammer :
     params -> bool -> int -> relevance_override -> (string -> minimize_command)
     -> Proof.state -> bool * Proof.state
@@ -410,30 +410,35 @@
   | failure_from_smt_failure (SMT_Solver.Counterexample _) = Unprovable
   | failure_from_smt_failure (SMT_Solver.Other_Failure _) = UnknownError
 
-fun run_smt_solver remote ({timeout, ...} : params) minimize_command
+fun run_smt_solver ctxt remote ({timeout, ...} : params) minimize_command
                    ({state, subgoal, subgoal_count, axioms, ...}
                     : prover_problem) =
   let
     val {outcome, used_facts, run_time_in_msecs} =
       SMT_Solver.smt_filter remote timeout state
                             (map_filter (try dest_Untranslated) axioms) subgoal
+    val outcome' = outcome |> Option.map failure_from_smt_failure (* FIXME *)
     val message =
-      if outcome = NONE then
+      case outcome of
+        NONE =>
         try_command_line (proof_banner false)
                          (apply_on_subgoal subgoal subgoal_count ^
                           command_call smtN (map fst used_facts)) ^
         minimize_line minimize_command (map fst used_facts)
-      else
-        ""
+      | SOME (SMT_Solver.Other_Failure message) => message
+      | SOME _ => string_for_failure (the outcome')
   in
-    {outcome = outcome |> Option.map failure_from_smt_failure,
-     used_axioms = used_facts, run_time_in_msecs = SOME run_time_in_msecs,
-     message = message}
+    {outcome = outcome', used_axioms = used_facts,
+     run_time_in_msecs = SOME run_time_in_msecs, message = message}
   end
 
-fun get_prover thy auto name =
-  if is_smt_prover name then run_smt_solver (String.isPrefix remote_prefix name)
-  else run_atp auto name (get_atp thy name)
+fun get_prover ctxt auto name =
+  let val thy = ProofContext.theory_of ctxt in
+    if is_smt_prover name then
+      run_smt_solver ctxt (String.isPrefix remote_prefix name)
+    else
+      run_atp auto name (get_atp thy name)
+  end
 
 fun run_prover (params as {blocking, debug, max_relevant, timeout, expect, ...})
                auto minimize_command
@@ -452,7 +457,7 @@
     fun go () =
       let
         fun really_go () =
-          get_prover thy auto name params (minimize_command name) problem
+          get_prover ctxt auto name params (minimize_command name) problem
           |> (fn {outcome, message, ...} =>
                  (if is_some outcome then "none" else "some", message))
         val (outcome_code, message) =

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Tue Oct 26 14:06:22 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Tue Oct 26 15:00:57 2010 +0200
@@ -92,7 +92,8 @@
                    state axioms =
   let
     val thy = Proof.theory_of state
-    val prover = get_prover thy false prover_name
+    val ctxt = Proof.context_of state
+    val prover = get_prover ctxt false prover_name
     val msecs = Time.toMilliseconds timeout
     val _ = Output.urgent_message ("Sledgehammer minimize: " ^ quote prover_name ^ ".")
     val {goal, ...} = Proof.goal state

--- a/src/Pure/Isar/code.ML	Tue Oct 26 14:06:22 2010 +0200
+++ b/src/Pure/Isar/code.ML	Tue Oct 26 15:00:57 2010 +0200
@@ -542,7 +542,7 @@
     val (rep, lhs) = dest_comb full_lhs
       handle TERM _ => bad "Not an abstract equation";
     val (rep_const, ty) = dest_Const rep;
-    val (tyco, sorts) = ((apsnd o map) (snd o dest_TVar) o dest_Type o domain_type) ty
+    val (tyco, Ts) = (dest_Type o domain_type) ty
       handle TERM _ => bad "Not an abstract equation"
            | TYPE _ => bad "Not an abstract equation";
     val _ = case some_tyco of SOME tyco' => if tyco = tyco' then ()
@@ -553,8 +553,8 @@
       else bad ("Projection mismatch: " ^ quote rep_const ^ " vs. " ^ quote rep');
     val _ = check_eqn thy { allow_nonlinear = false,
       allow_consts = false, allow_pats = false } thm (lhs, rhs);
-    val _ = if forall (Sign.subsort thy) (sorts ~~ map snd  vs') then ()
-      else error ("Sort constraints on type arguments are weaker than in abstype certificate.")
+    val _ = if forall (Sign.of_sort thy) (Ts ~~ map snd vs') then ()
+      else error ("Type arguments do not satisfy sort constraints of abstype certificate.");
   in (thm, tyco) end;
 
 fun assert_eqn thy = error_thm (gen_assert_eqn thy true);