summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

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