1.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Tue Nov 17 19:08:02 2009 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Tue Nov 17 19:12:10 2009 +0100
     1.3 @@ -1109,13 +1109,13 @@
     1.4      |> map_filter (try (Refute.specialize_type thy x))
     1.5      |> filter (equal (Const x) o term_under_def)
     1.6  
     1.7 -(* term -> term *)
     1.8 +(* theory -> term -> term option *)
     1.9  fun normalized_rhs_of thy t =
    1.10    let
    1.11 -    (* term -> term *)
    1.12 -    fun aux (v as Var _) t = lambda v t
    1.13 -      | aux (c as Const (@{const_name TYPE}, T)) t = lambda c t
    1.14 -      | aux _ _ = raise TERM ("Nitpick_HOL.normalized_rhs_of", [t])
    1.15 +    (* term option -> term option *)
    1.16 +    fun aux (v as Var _) (SOME t) = SOME (lambda v t)
    1.17 +      | aux (c as Const (@{const_name TYPE}, T)) (SOME t) = SOME (lambda c t)
    1.18 +      | aux _ _ = NONE
    1.19      val (lhs, rhs) =
    1.20        case t of
    1.21          Const (@{const_name "=="}, _) $ t1 $ t2 => (t1, t2)
    1.22 @@ -1123,7 +1123,7 @@
    1.23          (t1, t2)
    1.24        | _ => raise TERM ("Nitpick_HOL.normalized_rhs_of", [t])
    1.25      val args = strip_comb lhs |> snd
    1.26 -  in fold_rev aux args rhs end
    1.27 +  in fold_rev aux args (SOME rhs) end
    1.28  
    1.29  (* theory -> const_table -> styp -> term option *)
    1.30  fun def_of_const thy table (x as (s, _)) =
    1.31 @@ -1131,7 +1131,7 @@
    1.32      NONE
    1.33    else
    1.34      x |> def_props_for_const thy false table |> List.last
    1.35 -      |> normalized_rhs_of thy |> prefix_abs_vars s |> SOME
    1.36 +      |> normalized_rhs_of thy |> Option.map (prefix_abs_vars s)
    1.37      handle List.Empty => NONE
    1.38  
    1.39  datatype fixpoint_kind = Lfp | Gfp | NoFp