equal
deleted
inserted
replaced
76 in |
76 in |
77 if timeout = Time.zeroTime then |
77 if timeout = Time.zeroTime then |
78 dont_know () |
78 dont_know () |
79 else |
79 else |
80 let |
80 let |
81 val fact_names = used_facts |> map fst |> sort string_ord |
81 val fact_names = map fst used_facts |
82 |
82 |
83 val {context = ctxt, facts = chained, goal} = Proof.goal state |
83 val {context = ctxt, facts = chained, goal} = Proof.goal state |
84 val (_, hyp_ts, concl_t) = strip_subgoal goal i ctxt |
84 val (_, hyp_ts, concl_t) = strip_subgoal goal i ctxt |
85 val goal_t = Logic.list_implies (map prop_of chained @ hyp_ts, concl_t) |
85 val goal_t = Logic.list_implies (map prop_of chained @ hyp_ts, concl_t) |
86 |
86 |