# HG changeset patch
# User blanchet
# Date 1272452430 -7200
# Node ID 32c92af68ec9a77e36eea7661102efc0c0b9a52d
# Parent  50fd056cc3ce84f39481960649d8e231bf9f9eec
remove Sledgehammer's "sorts" option to annotate variables with sorts in proof;
what we need is smarter type annotations for variables _and_ constants

diff -r 50fd056cc3ce -r 32c92af68ec9 src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML	Wed Apr 28 12:49:52 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML	Wed Apr 28 13:00:30 2010 +0200
@@ -68,7 +68,7 @@
 (* minimalization of thms *)
 
 fun minimize_theorems (params as {debug, atps, minimize_timeout, isar_proof,
-                                  shrink_factor, sorts, ...})
+                                  shrink_factor, ...})
                       i n state name_thms_pairs =
   let
     val thy = Proof.theory_of state
@@ -109,8 +109,7 @@
         in
           (SOME min_thms,
            proof_text isar_proof
-                      (pool, debug, shrink_factor, sorts, ctxt,
-                       conjecture_shape)
+                      (pool, debug, shrink_factor, ctxt, conjecture_shape)
                       (K "", proof, internal_thm_names, goal, i) |> fst)
         end
     | {outcome = SOME TimedOut, ...} =>
diff -r 50fd056cc3ce -r 32c92af68ec9 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Wed Apr 28 12:49:52 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Wed Apr 28 13:00:30 2010 +0200
@@ -99,7 +99,6 @@
    ("follow_defs", "false"),
    ("isar_proof", "false"),
    ("shrink_factor", "1"),
-   ("sorts", "false"),
    ("minimize_timeout", "5 s")]
 
 val alias_params =
@@ -113,12 +112,11 @@
    ("ignore_no_atp", "respect_no_atp"),
    ("theory_irrelevant", "theory_relevant"),
    ("dont_follow_defs", "follow_defs"),
-   ("metis_proof", "isar_proof"),
-   ("no_sorts", "sorts")]
+   ("metis_proof", "isar_proof")]
 
 val params_for_minimize =
   ["debug", "verbose", "overlord", "full_types", "explicit_apply",
-   "isar_proof", "shrink_factor", "sorts", "minimize_timeout"]
+   "isar_proof", "shrink_factor", "minimize_timeout"]
 
 val property_dependent_params = ["atps", "full_types", "timeout"]
 
@@ -201,7 +199,6 @@
     val follow_defs = lookup_bool "follow_defs"
     val isar_proof = lookup_bool "isar_proof"
     val shrink_factor = Int.max (1, lookup_int "shrink_factor")
-    val sorts = lookup_bool "sorts"
     val timeout = lookup_time "timeout"
     val minimize_timeout = lookup_time "minimize_timeout"
   in
@@ -210,7 +207,7 @@
      respect_no_atp = respect_no_atp, relevance_threshold = relevance_threshold,
      convergence = convergence, theory_relevant = theory_relevant,
      follow_defs = follow_defs, isar_proof = isar_proof,
-     shrink_factor = shrink_factor, sorts = sorts, timeout = timeout,
+     shrink_factor = shrink_factor, timeout = timeout,
      minimize_timeout = minimize_timeout}
   end
 
diff -r 50fd056cc3ce -r 32c92af68ec9 src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Wed Apr 28 12:49:52 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Wed Apr 28 13:00:30 2010 +0200
@@ -21,11 +21,11 @@
     minimize_command * string * string vector * thm * int
     -> string * string list
   val isar_proof_text:
-    name_pool option * bool * int * bool * Proof.context * int list list
+    name_pool option * bool * int * Proof.context * int list list
     -> minimize_command * string * string vector * thm * int
     -> string * string list
   val proof_text:
-    bool -> name_pool option * bool * int * bool * Proof.context * int list list
+    bool -> name_pool option * bool * int * Proof.context * int list list
     -> minimize_command * string * string vector * thm * int
     -> string * string list
 end;
@@ -830,7 +830,7 @@
       | aux subst depth nextp (ps :: proof) = ps :: aux subst depth nextp proof
   in aux [] 0 (1, 1) end
 
-fun string_for_proof ctxt sorts i n =
+fun string_for_proof ctxt i n =
   let
     fun fix_print_mode f =
       PrintMode.setmp (filter (curry (op =) Symbol.xsymbolsN)
@@ -883,9 +883,9 @@
         do_indent 0 ^ "proof -\n" ^
         do_steps "" "" 1 proof ^
         do_indent 0 ^ (if n <> 1 then "next" else "qed") ^ "\n"
-  in setmp_CRITICAL show_sorts sorts do_proof end
+  in do_proof end
 
-fun isar_proof_text (pool, debug, shrink_factor, sorts, ctxt, conjecture_shape)
+fun isar_proof_text (pool, debug, shrink_factor, ctxt, conjecture_shape)
                     (minimize_command, atp_proof, thm_names, goal, i) =
   let
     val thy = ProofContext.theory_of ctxt
@@ -901,7 +901,7 @@
            |> then_chain_proof
            |> kill_useless_labels_in_proof
            |> relabel_proof
-           |> string_for_proof ctxt sorts i n of
+           |> string_for_proof ctxt i n of
         "" => ""
       | proof => "\nStructured proof:\n" ^ Markup.markup Markup.sendback proof
     val isar_proof =