src/HOL/Tools/Nitpick/nitpick_hol.ML
changeset 33705 947184dc75c9
parent 33583 b5e0909cd5ea
child 33706 7017aee615d6
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Fri Nov 13 06:24:31 2009 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Fri Nov 13 15:59:53 2009 +0100
@@ -7,6 +7,7 @@
 
 signature NITPICK_HOL =
 sig
+  type styp = Nitpick_Util.styp
   type const_table = term list Symtab.table
   type special_fun = (styp * int list * term list) * styp
   type unrolled = styp * styp
@@ -1499,7 +1500,7 @@
               SOME n =>
               let
                 val (dataT, res_T) = nth_range_type n T
-                                     |> domain_type pairf range_type
+                                     |> pairf domain_type range_type
               in
                 (optimized_case_def ext_ctxt dataT res_T
                  |> do_term (depth + 1) Ts, ts)
@@ -1675,8 +1676,8 @@
          | NONE =>
            let
              val goal = prop |> cterm_of thy |> Goal.init
-             val wf = silence (exists (terminates_by ctxt tac_timeout goal))
-                              termination_tacs
+             val wf = exists (terminates_by ctxt tac_timeout goal)
+                             termination_tacs
            in Unsynchronized.change cached_wf_props (cons (prop, wf)); wf end
        end)
     handle List.Empty => false