merged
authorwenzelm
Tue, 26 Oct 2010 11:06:12 +0200
changeset 40148 8728165d366e
parent 40147 d170c322157a (diff)
parent 40134 8baded087d34 (current diff)
child 40149 4c35be108990
merged
src/Tools/quickcheck.ML
--- a/doc-src/Nitpick/nitpick.tex	Mon Oct 25 22:47:02 2010 +0200
+++ b/doc-src/Nitpick/nitpick.tex	Tue Oct 26 11:06:12 2010 +0200
@@ -1751,7 +1751,7 @@
 {\slshape Nitpick ran out of time after checking 9 of 10 scopes.}
 \postw
 
-Furthermore, applying \textit{skew} or \textit{split} to a well-formed tree
+Furthermore, applying \textit{skew} or \textit{split} on a well-formed tree
 should not alter the tree:
 
 \prew
@@ -1802,10 +1802,10 @@
 \postw
 
 Nitpick's output reveals that the element $0$ was added as a left child of $1$,
-where both have a level of 1. This violates the second AA tree invariant, which
-states that a left child's level must be less than its parent's. This shouldn't
-come as a surprise, considering that we commented out the tree rebalancing code.
-Reintroducing the code seems to solve the problem:
+where both nodes have a level of 1. This violates the second AA tree invariant,
+which states that a left child's level must be less than its parent's. This
+shouldn't come as a surprise, considering that we commented out the tree
+rebalancing code. Reintroducing the code seems to solve the problem:
 
 \prew
 \textbf{theorem}~\textit{wf\_insort\/}:\kern.4em ``$\textit{wf}~t\,\Longrightarrow\, \textit{wf}~(\textit{insort}~t~x)$'' \\
--- a/src/HOL/IsaMakefile	Mon Oct 25 22:47:02 2010 +0200
+++ b/src/HOL/IsaMakefile	Tue Oct 26 11:06:12 2010 +0200
@@ -306,12 +306,15 @@
   Tools/numeral.ML \
   Tools/numeral_simprocs.ML \
   Tools/numeral_syntax.ML \
+  Tools/Predicate_Compile/core_data.ML \
+  Tools/Predicate_Compile/mode_inference.ML \
   Tools/Predicate_Compile/predicate_compile_aux.ML \
   Tools/Predicate_Compile/predicate_compile_compilations.ML \
   Tools/Predicate_Compile/predicate_compile_core.ML \
   Tools/Predicate_Compile/predicate_compile_data.ML \
   Tools/Predicate_Compile/predicate_compile_fun.ML \
   Tools/Predicate_Compile/predicate_compile.ML \
+  Tools/Predicate_Compile/predicate_compile_proof.ML \
   Tools/Predicate_Compile/predicate_compile_specialisation.ML \
   Tools/Predicate_Compile/predicate_compile_pred.ML \
   Tools/quickcheck_generators.ML \
--- a/src/HOL/Predicate_Compile_Examples/Hotel_Example_Prolog.thy	Mon Oct 25 22:47:02 2010 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Hotel_Example_Prolog.thy	Tue Oct 26 11:06:12 2010 +0200
@@ -23,7 +23,7 @@
 setup {* Context.theory_map (Quickcheck.add_generator ("prolog", Code_Prolog.quickcheck)) *}
 
 lemma "\<lbrakk> hotel s; g \<in> isin s r \<rbrakk> \<Longrightarrow> owns s r = Some g"
-quickcheck[generator = code, iterations = 100000, report]
+quickcheck[generator = code, iterations = 10000, report]
 quickcheck[generator = prolog, iterations = 1, expect = counterexample]
 oops
 
--- a/src/HOL/Predicate_Compile_Examples/Hotel_Example_Small_Generator.thy	Mon Oct 25 22:47:02 2010 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Hotel_Example_Small_Generator.thy	Tue Oct 26 11:06:12 2010 +0200
@@ -5,6 +5,12 @@
 
 declare Let_def[code_pred_inline]
 
+lemma [code_pred_inline]: "insert == (%y A x. y = x | A x)"
+by (auto simp add: insert_iff[unfolded mem_def] fun_eq_iff intro!: eq_reflection)
+
+lemma [code_pred_inline]: "(op -) == (%A B x. A x \<and> \<not> B x)"
+by (auto simp add: Diff_iff[unfolded mem_def] fun_eq_iff intro!: eq_reflection)
+
 instantiation room :: small_lazy
 begin
 
@@ -44,8 +50,8 @@
 
 lemma
   "hotel s ==> feels_safe s r ==> g \<in> isin s r ==> owns s r = Some g"
-quickcheck[generator = small_generators_depth_14, iterations = 1, expect = no_counterexample]
-quickcheck[generator = small_generators_depth_15, iterations = 1, expect = counterexample]
+quickcheck[generator = small_generators_depth_14, iterations = 1, size = 1, expect = no_counterexample]
+quickcheck[generator = small_generators_depth_15, iterations = 1, size = 1, expect = counterexample]
 oops
 
 
--- a/src/HOL/Predicate_Compile_Examples/List_Examples.thy	Mon Oct 25 22:47:02 2010 +0200
+++ b/src/HOL/Predicate_Compile_Examples/List_Examples.thy	Tue Oct 26 11:06:12 2010 +0200
@@ -16,7 +16,7 @@
    manual_reorder = []}) *}
 
 lemma "(xs :: nat list) = ys @ ys --> rev xs = xs"
-quickcheck[generator = code, iterations = 200000, expect = counterexample]
+quickcheck[generator = code, iterations = 10000]
 quickcheck[generator = predicate_compile_wo_ff, iterations = 1, expect = counterexample]
 quickcheck[generator = prolog, expect = counterexample]
 oops
--- a/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy	Mon Oct 25 22:47:02 2010 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy	Tue Oct 26 11:06:12 2010 +0200
@@ -974,9 +974,10 @@
 
 code_pred [new_random_dseq inductify] avl .
 thm avl.new_random_dseq_equation
+(* TODO: has highly non-deterministic execution time!
 
 values [new_random_dseq 2, 1, 7] 5 "{t:: int tree. avl t}"
-
+*)
 fun set_of
 where
 "set_of ET = {}"
--- a/src/HOL/Predicate_Compile_Examples/ROOT.ML	Mon Oct 25 22:47:02 2010 +0200
+++ b/src/HOL/Predicate_Compile_Examples/ROOT.ML	Tue Oct 26 11:06:12 2010 +0200
@@ -5,9 +5,9 @@
   "Specialisation_Examples",
   "Hotel_Example_Small_Generator",
   "IMP_1",
-  "IMP_2",
-  "IMP_3",
-  "IMP_4"];
+  "IMP_2"
+(*  "IMP_3",
+  "IMP_4"*)];
 
 if getenv "EXEC_SWIPL" = "" andalso getenv "EXEC_YAP" = "" then
   (warning "No prolog system found - skipping some example theories"; ())
--- a/src/HOL/Tools/Metis/metis_translate.ML	Mon Oct 25 22:47:02 2010 +0200
+++ b/src/HOL/Tools/Metis/metis_translate.ML	Tue Oct 26 11:06:12 2010 +0200
@@ -68,7 +68,7 @@
   val combtyp_of : combterm -> combtyp
   val strip_combterm_comb : combterm -> combterm * combterm list
   val combterm_from_term :
-    theory -> int -> (string * typ) list -> term -> combterm * typ list
+    theory -> (string * typ) list -> term -> combterm * typ list
   val reveal_old_skolem_terms : (string * term) list -> term -> term
   val tfree_classes_of_terms : term list -> string list
   val tvar_classes_of_terms : term list -> string list
@@ -215,10 +215,9 @@
     (s, Sign.the_const_type thy s) |> Sign.const_typargs thy |> length
 
 fun new_skolem_var_from_const s =
-  let
-    val ss = s |> space_explode Long_Name.separator
-    val n = length ss
-  in (nth ss (n - 2), nth ss (n - 3) |> Int.fromString |> the) end
+  let val ss = s |> space_explode Long_Name.separator in
+    (nth ss (length ss - 2), 0)
+  end
 
 
 (**** Definitions and functions for FOL clauses for TPTP format output ****)
@@ -396,17 +395,18 @@
   | simple_combtype_of (TVar (x, _)) =
     CombTVar (make_schematic_type_var x, string_of_indexname x)
 
-fun new_skolem_const_name th_no s num_T_args =
-  [new_skolem_const_prefix, string_of_int th_no, s, string_of_int num_T_args]
+fun new_skolem_const_name s num_T_args =
+  [new_skolem_const_prefix, s, string_of_int num_T_args]
   |> space_implode Long_Name.separator
 
-(* Converts a term (with combinators) into a combterm. Also accummulates sort
+(* Converts a term (with combinators) into a combterm. Also accumulates sort
    infomation. *)
-fun combterm_from_term thy th_no bs (P $ Q) =
-      let val (P', tsP) = combterm_from_term thy th_no bs P
-          val (Q', tsQ) = combterm_from_term thy th_no bs Q
-      in  (CombApp (P', Q'), union (op =) tsP tsQ)  end
-  | combterm_from_term thy _ _ (Const (c, T)) =
+fun combterm_from_term thy bs (P $ Q) =
+      let
+        val (P', tsP) = combterm_from_term thy bs P
+        val (Q', tsQ) = combterm_from_term thy bs Q
+      in (CombApp (P', Q'), union (op =) tsP tsQ) end
+  | combterm_from_term thy _ (Const (c, T)) =
       let
         val (tp, ts) = combtype_of T
         val tvar_list =
@@ -417,43 +417,42 @@
           |> map simple_combtype_of
         val c' = CombConst (`make_fixed_const c, tp, tvar_list)
       in  (c',ts)  end
-  | combterm_from_term _ _ _ (Free (v, T)) =
+  | combterm_from_term _ _ (Free (v, T)) =
       let val (tp, ts) = combtype_of T
           val v' = CombConst (`make_fixed_var v, tp, [])
       in  (v',ts)  end
-  | combterm_from_term _ th_no _ (Var (v as (s, _), T)) =
+  | combterm_from_term _ _ (Var (v as (s, _), T)) =
     let
       val (tp, ts) = combtype_of T
       val v' =
         if String.isPrefix Meson_Clausify.new_skolem_var_prefix s then
           let
             val tys = T |> strip_type |> swap |> op ::
-            val s' = new_skolem_const_name th_no s (length tys)
+            val s' = new_skolem_const_name s (length tys)
           in
             CombConst (`make_fixed_const s', tp, map simple_combtype_of tys)
           end
         else
           CombVar ((make_schematic_var v, string_of_indexname v), tp)
     in (v', ts) end
-  | combterm_from_term _ _ bs (Bound j) =
+  | combterm_from_term _ bs (Bound j) =
       let
         val (s, T) = nth bs j
         val (tp, ts) = combtype_of T
         val v' = CombConst (`make_bound_var s, tp, [])
       in (v', ts) end
-  | combterm_from_term _ _ _ (Abs _) = raise Fail "HOL clause: Abs"
+  | combterm_from_term _ _ (Abs _) = raise Fail "HOL clause: Abs"
 
-fun predicate_of thy th_no ((@{const Not} $ P), pos) =
-    predicate_of thy th_no (P, not pos)
-  | predicate_of thy th_no (t, pos) =
-    (combterm_from_term thy th_no [] (Envir.eta_contract t), pos)
+fun predicate_of thy ((@{const Not} $ P), pos) = predicate_of thy (P, not pos)
+  | predicate_of thy (t, pos) =
+    (combterm_from_term thy [] (Envir.eta_contract t), pos)
 
-fun literals_of_term1 args thy th_no (@{const Trueprop} $ P) =
-    literals_of_term1 args thy th_no P
-  | literals_of_term1 args thy th_no (@{const HOL.disj} $ P $ Q) =
-    literals_of_term1 (literals_of_term1 args thy th_no P) thy th_no Q
-  | literals_of_term1 (lits, ts) thy th_no P =
-    let val ((pred, ts'), pol) = predicate_of thy th_no (P, true) in
+fun literals_of_term1 args thy (@{const Trueprop} $ P) =
+    literals_of_term1 args thy P
+  | literals_of_term1 args thy (@{const HOL.disj} $ P $ Q) =
+    literals_of_term1 (literals_of_term1 args thy P) thy Q
+  | literals_of_term1 (lits, ts) thy P =
+    let val ((pred, ts'), pol) = predicate_of thy (P, true) in
       (FOLLiteral (pol, pred) :: lits, union (op =) ts ts')
     end
 val literals_of_term = literals_of_term1 ([], [])
@@ -607,9 +606,10 @@
             metis_lit pos "=" (map hol_term_to_fol_FT tms)
         | _ => metis_lit pos "{}" [hol_term_to_fol_FT tm])   (*hBOOL*);
 
-fun literals_of_hol_term thy th_no mode t =
-      let val (lits, types_sorts) = literals_of_term thy th_no t
-      in  (map (hol_literal_to_fol mode) lits, types_sorts) end;
+fun literals_of_hol_term thy mode t =
+  let val (lits, types_sorts) = literals_of_term thy t in
+    (map (hol_literal_to_fol mode) lits, types_sorts)
+  end
 
 (*Sign should be "true" for conjecture type constraints, "false" for type lits in clauses.*)
 fun metis_of_type_literals pos (TyLitVar ((s, _), (s', _))) =
@@ -623,13 +623,13 @@
 fun metis_of_tfree tf =
   Metis_Thm.axiom (Metis_LiteralSet.singleton (metis_of_type_literals true tf));
 
-fun hol_thm_to_fol is_conjecture th_no ctxt type_lits mode j old_skolems th =
+fun hol_thm_to_fol is_conjecture ctxt type_lits mode j old_skolems th =
   let
     val thy = ProofContext.theory_of ctxt
     val (old_skolems, (mlits, types_sorts)) =
      th |> prop_of |> Logic.strip_imp_concl
         |> conceal_old_skolem_terms j old_skolems
-        ||> (HOLogic.dest_Trueprop #> literals_of_hol_term thy th_no mode)
+        ||> (HOLogic.dest_Trueprop #> literals_of_hol_term thy mode)
   in
     if is_conjecture then
       (Metis_Thm.axiom (Metis_LiteralSet.fromList mlits),
@@ -732,21 +732,20 @@
         | set_mode FT = FT
       val mode = set_mode mode0
       (*transform isabelle clause to metis clause *)
-      fun add_thm th_no is_conjecture (metis_ith, isa_ith)
+      fun add_thm is_conjecture (metis_ith, isa_ith)
                   {axioms, tfrees, old_skolems} : logic_map =
         let
           val (mth, tfree_lits, old_skolems) =
-            hol_thm_to_fol is_conjecture th_no ctxt type_lits mode (length axioms)
+            hol_thm_to_fol is_conjecture ctxt type_lits mode (length axioms)
                            old_skolems metis_ith
         in
            {axioms = (mth, Meson.make_meta_clause isa_ith) :: axioms,
             tfrees = union (op =) tfree_lits tfrees, old_skolems = old_skolems}
         end;
       val lmap = {axioms = [], tfrees = init_tfrees ctxt, old_skolems = []}
-                 |> fold (add_thm 0 true o `I) cls
+                 |> fold (add_thm true o `I) cls
                  |> add_tfrees
-                 |> fold (fn (th_no, ths) => fold (add_thm th_no false o `I) ths)
-                         (1 upto length thss ~~ thss)
+                 |> fold (fold (add_thm false o `I)) thss
       val clause_lists = map (Metis_Thm.clause o #1) (#axioms lmap)
       fun is_used c =
         exists (Metis_LiteralSet.exists (const_in_metis c o #2)) clause_lists
@@ -763,7 +762,7 @@
                                     []
                                   else
                                     thms)
-          in lmap |> fold (add_thm ~1 false) helper_ths end
+          in lmap |> fold (add_thm false) helper_ths end
   in
     (mode, add_type_thm (type_ext thy (maps (map prop_of) (cls :: thss))) lmap)
   end
--- a/src/HOL/Tools/Nitpick/nitpick_mono.ML	Mon Oct 25 22:47:02 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML	Tue Oct 26 11:06:12 2010 +0200
@@ -505,29 +505,29 @@
   end
 
 fun solve max_var (lits, comps, sexps) =
-    let
-      fun do_assigns assigns =
-        SOME (literals_from_assignments max_var assigns lits
-              |> tap print_solution)
-      val _ = print_problem lits comps sexps
-      val prop = PropLogic.all (map prop_for_literal lits @
-                                map prop_for_comp comps @
-                                map prop_for_sign_expr sexps)
-      val default_val = bool_from_sign Minus
-    in
-      if PropLogic.eval (K default_val) prop then
-        do_assigns (K (SOME default_val))
-      else
-        let
-          (* use the first ML solver (to avoid startup overhead) *)
-          val solvers = !SatSolver.solvers
-                        |> filter (member (op =) ["dptsat", "dpll"] o fst)
-        in
-          case snd (hd solvers) prop of
-            SatSolver.SATISFIABLE assigns => do_assigns assigns
-          | _ => NONE
-        end
-    end
+  let
+    fun do_assigns assigns =
+      SOME (literals_from_assignments max_var assigns lits
+            |> tap print_solution)
+    val _ = print_problem lits comps sexps
+    val prop = PropLogic.all (map prop_for_literal lits @
+                              map prop_for_comp comps @
+                              map prop_for_sign_expr sexps)
+    val default_val = bool_from_sign Minus
+  in
+    if PropLogic.eval (K default_val) prop then
+      do_assigns (K (SOME default_val))
+    else
+      let
+        (* use the first ML solver (to avoid startup overhead) *)
+        val solvers = !SatSolver.solvers
+                      |> filter (member (op =) ["dptsat", "dpll"] o fst)
+      in
+        case snd (hd solvers) prop of
+          SatSolver.SATISFIABLE assigns => do_assigns assigns
+        | _ => NONE
+      end
+  end
 
 type mtype_schema = mtyp * constraint_set
 type mtype_context =
--- a/src/HOL/Tools/Predicate_Compile/core_data.ML	Mon Oct 25 22:47:02 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/core_data.ML	Tue Oct 26 11:06:12 2010 +0200
@@ -186,7 +186,7 @@
 
 fun lookup_predfun_data ctxt name mode =
   Option.map rep_predfun_data
-    (AList.lookup (op =) (#predfun_data (the_pred_data ctxt name)) mode)
+    (AList.lookup eq_mode (#predfun_data (the_pred_data ctxt name)) mode)
 
 fun the_predfun_data ctxt name mode =
   case lookup_predfun_data ctxt name mode of
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Mon Oct 25 22:47:02 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Tue Oct 26 11:06:12 2010 +0200
@@ -35,7 +35,7 @@
   val split_map_modeT : (mode -> typ -> typ option * typ option)
     -> mode -> typ list -> typ list * typ list
   val split_mode : mode -> term list -> term list * term list
-  val split_modeT' : mode -> typ list -> typ list * typ list
+  val split_modeT : mode -> typ list -> typ list * typ list
   val string_of_mode : mode -> string
   val ascii_string_of_mode : mode -> string
   (* premises *)
@@ -393,24 +393,22 @@
 fun map_filter_prod f (Const (@{const_name Pair}, _) $ t1 $ t2) =
   comb_option HOLogic.mk_prod (map_filter_prod f t1, map_filter_prod f t2)
   | map_filter_prod f t = f t
-
-(* obviously, split_mode' and split_modeT' do not match? where does that cause problems? *)
   
-fun split_modeT' mode Ts =
+fun split_modeT mode Ts =
   let
-    fun split_arg_mode' (Fun _) T = ([], [])
-      | split_arg_mode' (Pair (m1, m2)) (Type (@{type_name Product_Type.prod}, [T1, T2])) =
+    fun split_arg_mode (Fun _) T = ([], [])
+      | split_arg_mode (Pair (m1, m2)) (Type (@{type_name Product_Type.prod}, [T1, T2])) =
         let
-          val (i1, o1) = split_arg_mode' m1 T1
-          val (i2, o2) = split_arg_mode' m2 T2
+          val (i1, o1) = split_arg_mode m1 T1
+          val (i2, o2) = split_arg_mode m2 T2
         in
           (i1 @ i2, o1 @ o2)
         end
-      | split_arg_mode' Input T = ([T], [])
-      | split_arg_mode' Output T = ([], [T])
-      | split_arg_mode' _ _ = raise Fail "split_modeT': mode and type do not match"
+      | split_arg_mode Input T = ([T], [])
+      | split_arg_mode Output T = ([], [T])
+      | split_arg_mode _ _ = raise Fail "split_modeT: mode and type do not match"
   in
-    (pairself flat o split_list) (map2 split_arg_mode' (strip_fun_mode mode) Ts)
+    (pairself flat o split_list) (map2 split_arg_mode (strip_fun_mode mode) Ts)
   end
 
 fun string_of_mode mode =
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Mon Oct 25 22:47:02 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Tue Oct 26 11:06:12 2010 +0200
@@ -167,7 +167,7 @@
 
 (* validity checks *)
 
-fun check_expected_modes preds options modes =
+fun check_expected_modes options preds modes =
   case expected_modes options of
     SOME (s, ms) => (case AList.lookup (op =) modes s of
       SOME modes =>
@@ -183,7 +183,7 @@
       | NONE => ())
   | NONE => ()
 
-fun check_proposed_modes preds options modes errors =
+fun check_proposed_modes options preds modes errors =
   map (fn (s, _) => case proposed_modes options s of
     SOME ms => (case AList.lookup (op =) modes s of
       SOME inferred_ms =>
@@ -319,7 +319,7 @@
     fn compfuns => fn s => fn T => fn mode => fn additional_arguments => fn compilation =>
     let
       val [depth] = additional_arguments
-      val (_, Ts) = split_modeT' mode (binder_types T)
+      val (_, Ts) = split_modeT mode (binder_types T)
       val T' = mk_predT compfuns (HOLogic.mk_tupleT Ts)
       val if_const = Const (@{const_name "If"}, @{typ bool} --> T' --> T' --> T')
     in
@@ -1379,8 +1379,8 @@
         options (lookup_mode, lookup_neg_mode, needs_random) ctxt preds all_modes param_vs clauses)
     val thy' = fold (fn (s, ms) => set_needs_random s ms) needs_random thy
     val modes = map (fn (p, mps) => (p, map fst mps)) moded_clauses
-    val _ = check_expected_modes preds options modes
-    val _ = check_proposed_modes preds options modes errors
+    val _ = check_expected_modes options preds modes
+    val _ = check_proposed_modes options preds modes errors
     val _ = print_modes options modes
     val _ = print_step options "Defining executable functions..."
     val thy'' =
@@ -1799,7 +1799,7 @@
         mk_map compfuns T HOLogic.termT (HOLogic.term_of_const T) t
     val thy = ProofContext.theory_of ctxt
     val (ts, statistics) =
-      case compilation of
+      (case compilation of
        (* Random =>
           fst (Predicate.yieldn k
           (Code_Eval.eval NONE ("Predicate_Compile_Core.random_eval_ref", random_eval_ref)
@@ -1809,25 +1809,25 @@
           let
             val [nrandom, size, depth] = arguments
           in
-            rpair NONE (fst (DSequence.yieldn k
+            rpair NONE (TimeLimit.timeLimit (Time.fromSeconds 20) (fn () => fst (DSequence.yieldn k
               (Code_Runtime.dynamic_value_strict (Dseq_Random_Result.get, put_dseq_random_result, "Predicate_Compile_Core.put_dseq_random_result")
                 thy NONE (fn proc => fn g => fn nrandom => fn size => fn s => g nrandom size s |>> DSequence.map proc)
                   t' [] nrandom size
                 |> Random_Engine.run)
-              depth true))
+              depth true)) ())
           end
       | DSeq =>
-          rpair NONE (fst (DSequence.yieldn k
+          rpair NONE (TimeLimit.timeLimit (Time.fromSeconds 20) (fn () => fst (DSequence.yieldn k
             (Code_Runtime.dynamic_value_strict (Dseq_Result.get, put_dseq_result, "Predicate_Compile_Core.put_dseq_result")
-              thy NONE DSequence.map t' []) (the_single arguments) true))
+              thy NONE DSequence.map t' []) (the_single arguments) true)) ())
       | Pos_Generator_DSeq =>
           let
             val depth = (the_single arguments)
           in
-            rpair NONE (fst (Lazy_Sequence.yieldn k
+            rpair NONE (TimeLimit.timeLimit (Time.fromSeconds 20) (fn () => fst (Lazy_Sequence.yieldn k
               (Code_Runtime.dynamic_value_strict (New_Dseq_Result.get, put_new_dseq_result, "Predicate_Compile_Core.put_new_dseq_result")
               thy NONE (fn proc => fn g => fn depth => g depth |> Lazy_Sequence.mapa proc)
-              t' [] depth)))
+              t' [] depth))) ())
           end
       | New_Pos_Random_DSeq =>
           let
@@ -1835,27 +1835,28 @@
             val seed = Random_Engine.next_seed ()
           in
             if stats then
-              apsnd (SOME o accumulate) (split_list
-              (fst (Lazy_Sequence.yieldn k
+              apsnd (SOME o accumulate) (split_list (TimeLimit.timeLimit (Time.fromSeconds 20)
+              (fn () => fst (Lazy_Sequence.yieldn k
                 (Code_Runtime.dynamic_value_strict
                   (Lseq_Random_Stats_Result.get, put_lseq_random_stats_result, "Predicate_Compile_Core.put_lseq_random_stats_result")
                   thy NONE
                   (fn proc => fn g => fn nrandom => fn size => fn s => fn depth => g nrandom size s depth
                     |> Lazy_Sequence.mapa (apfst proc))
-                    t' [] nrandom size seed depth))))
+                    t' [] nrandom size seed depth))) ()))
             else rpair NONE
-              (fst (Lazy_Sequence.yieldn k
+              (TimeLimit.timeLimit (Time.fromSeconds 20) (fn () => fst (Lazy_Sequence.yieldn k
                 (Code_Runtime.dynamic_value_strict
                   (Lseq_Random_Result.get, put_lseq_random_result, "Predicate_Compile_Core.put_lseq_random_result")
                   thy NONE 
                   (fn proc => fn g => fn nrandom => fn size => fn s => fn depth => g nrandom size s depth
                     |> Lazy_Sequence.mapa proc)
-                    t' [] nrandom size seed depth)))
+                    t' [] nrandom size seed depth))) ())
           end
       | _ =>
-          rpair NONE (fst (Predicate.yieldn k
+          rpair NONE (TimeLimit.timeLimit (Time.fromSeconds 20) (fn () => fst (Predicate.yieldn k
             (Code_Runtime.dynamic_value_strict (Pred_Result.get, put_pred_result, "Predicate_Compile_Core.put_pred_result")
-              thy NONE Predicate.map t' [])))
+              thy NONE Predicate.map t' []))) ()))
+     handle TimeLimit.TimeOut => error "Reached timeout during execution of values"
   in ((T, ts), statistics) end;
 
 fun values ctxt param_user_modes ((raw_expected, stats), comp_options) k t_compr =
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML	Mon Oct 25 22:47:02 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML	Tue Oct 26 11:06:12 2010 +0200
@@ -74,6 +74,11 @@
 *)
 val defining_term_of_introrule = defining_term_of_introrule_term o prop_of
 
+fun defining_const_of_introrule th =
+  case defining_term_of_introrule th
+   of Const (c, _) => c
+    | _ => raise TERM ("defining_const_of_introrule failed: Not a constant", [prop_of th])
+
 (*TODO*)
 fun is_introlike_term t = true
 
@@ -194,7 +199,7 @@
         defining_const_of_equation (normalize_equation thy th) = fst (dest_Const t) then
         SOME (normalize_equation thy th)
       else
-        if is_introlike th andalso defining_term_of_introrule th = t then
+        if is_introlike th andalso defining_const_of_introrule th = fst (dest_Const t) then
           SOME th
         else
           NONE
@@ -206,7 +211,8 @@
     | ths => rev ths
     val _ =
       if show_intermediate_results options then
-        Output.tracing (commas (map (Display.string_of_thm_global thy) spec))
+        Output.tracing ("Specification for " ^ (Syntax.string_of_term_global thy t) ^ ":\n" ^
+          commas (map (Display.string_of_thm_global thy) spec))
       else ()
   in
     spec
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Mon Oct 25 22:47:02 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Tue Oct 26 11:06:12 2010 +0200
@@ -53,7 +53,7 @@
 
 fun combformula_for_prop thy =
   let
-    val do_term = combterm_from_term thy ~1
+    val do_term = combterm_from_term thy
     fun do_quant bs q s T t' =
       let val s = Name.variant (map fst bs) s in
         do_formula ((s, T) :: bs) t'
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Mon Oct 25 22:47:02 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Tue Oct 26 11:06:12 2010 +0200
@@ -157,7 +157,7 @@
       prover :: avoid_too_many_local_threads thy n provers
     end
 
-val num_processors = try Thread.numProcessors #> the_default 1
+fun num_processors () = try Thread.numProcessors () |> the_default 1
 
 (* The first ATP of the list is used by Auto Sledgehammer. Because of the low
    timeout, it makes sense to put SPASS first. *)
@@ -362,6 +362,6 @@
                        (minimize_command [] 1) state
     end
 
-val setup = Auto_Tools.register_tool ("sledgehammer", auto_sledgehammer)
+val setup = Auto_Tools.register_tool (sledgehammerN, auto_sledgehammer)
 
 end;
--- a/src/Tools/quickcheck.ML	Mon Oct 25 22:47:02 2010 +0200
+++ b/src/Tools/quickcheck.ML	Tue Oct 26 11:06:12 2010 +0200
@@ -196,10 +196,12 @@
           val (result, new_report) = with_testers k testers
           val reports = ((k, new_report) :: reports)
         in case result of NONE => with_size (k + 1) reports | SOME q => (SOME q, reports) end);
-    val ((result, reports), exec_time) = cpu_time "quickcheck execution"
+    val ((result, reports), exec_time) =
+      TimeLimit.timeLimit (Time.fromSeconds 20) (fn () => cpu_time "quickcheck execution"
       (fn () => apfst
          (fn result => case result of NONE => NONE
-        | SOME ts => SOME (names ~~ ts)) (with_size 1 []))
+        | SOME ts => SOME (names ~~ ts)) (with_size 1 []))) ()
+      handle TimeLimit.TimeOut => error "Reached timeout during Quickcheck"
   in
     (result, ([exec_time, comp_time], if report ctxt then SOME reports else NONE))
   end;