src/HOL/Tools/Nitpick/nitpick_hol.ML
changeset 33706 7017aee615d6
parent 33701 9dd1079cec3a
parent 33705 947184dc75c9
child 33743 a58893035742
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Sun Nov 15 21:58:40 2009 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Mon Nov 16 10:03:58 2009 +0100
     1.3 @@ -7,6 +7,7 @@
     1.4  
     1.5  signature NITPICK_HOL =
     1.6  sig
     1.7 +  type styp = Nitpick_Util.styp
     1.8    type const_table = term list Symtab.table
     1.9    type special_fun = (styp * int list * term list) * styp
    1.10    type unrolled = styp * styp
    1.11 @@ -1499,7 +1500,7 @@
    1.12                SOME n =>
    1.13                let
    1.14                  val (dataT, res_T) = nth_range_type n T
    1.15 -                                     |> domain_type pairf range_type
    1.16 +                                     |> pairf domain_type range_type
    1.17                in
    1.18                  (optimized_case_def ext_ctxt dataT res_T
    1.19                   |> do_term (depth + 1) Ts, ts)
    1.20 @@ -1675,8 +1676,8 @@
    1.21           | NONE =>
    1.22             let
    1.23               val goal = prop |> cterm_of thy |> Goal.init
    1.24 -             val wf = silence (exists (terminates_by ctxt tac_timeout goal))
    1.25 -                              termination_tacs
    1.26 +             val wf = exists (terminates_by ctxt tac_timeout goal)
    1.27 +                             termination_tacs
    1.28             in Unsynchronized.change cached_wf_props (cons (prop, wf)); wf end
    1.29         end)
    1.30      handle List.Empty => false