src/HOL/Tools/Nitpick/nitpick.ML
changeset 59582 0fbed69ff081
parent 59432 42b7b76b37b8
child 59970 e9f73d87d904
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick.ML	Tue Mar 03 19:08:04 2015 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick.ML	Wed Mar 04 19:53:18 2015 +0100
     1.3 @@ -1065,14 +1065,14 @@
     1.4  fun pick_nits_in_subgoal state params mode i step =
     1.5    let
     1.6      val ctxt = Proof.context_of state
     1.7 -    val t = state |> Proof.raw_goal |> #goal |> prop_of
     1.8 +    val t = state |> Proof.raw_goal |> #goal |> Thm.prop_of
     1.9    in
    1.10      case Logic.count_prems t of
    1.11        0 => (writeln "No subgoal!"; (noneN, []))
    1.12      | n =>
    1.13        let
    1.14          val t = Logic.goal_params t i |> fst
    1.15 -        val assms = map term_of (Assumption.all_assms_of ctxt)
    1.16 +        val assms = map Thm.term_of (Assumption.all_assms_of ctxt)
    1.17          val (subst, assms, t) = extract_fixed_frees ctxt (assms, t)
    1.18        in pick_nits_in_term state params mode i n step subst [] assms t end
    1.19    end