equal
deleted
inserted
replaced
153 | subgoals n = "goal (" ^ string_of_int n ^ " subgoals):" |
153 | subgoals n = "goal (" ^ string_of_int n ^ " subgoals):" |
154 |
154 |
155 val state = proof_state node; |
155 val state = proof_state node; |
156 val goals = Pretty.chunks (Proof.pretty_goals false state); |
156 val goals = Pretty.chunks (Proof.pretty_goals false state); |
157 |
157 |
158 val {prop, ...} = rep_thm (Proof.get_goal state |> snd |> snd); |
158 val {prop, ...} = (rep_thm o #goal o Proof.goal) state; |
159 val (As, _) = Logic.strip_horn prop; |
159 val (As, _) = Logic.strip_horn prop; |
160 val output = (case (length As) of |
160 val output = (case (length As) of |
161 0 => [goals] |
161 0 => [goals] |
162 | n => [Pretty.str (subgoals n), goals]) |
162 | n => [Pretty.str (subgoals n), goals]) |
163 in |
163 in |
165 end |
165 end |
166 |
166 |
167 fun output_raw_goal_state {state = node, context = ctxt, ...} _ = |
167 fun output_raw_goal_state {state = node, context = ctxt, ...} _ = |
168 let |
168 let |
169 val state = proof_state node; |
169 val state = proof_state node; |
170 val goals = (Proof.get_goal state |> snd |> snd) |
170 val goals = (#goal o Proof.goal) state; |
171 |
171 |
172 val output = [Pretty.str (Syntax.string_of_term ctxt (prop_of goals))] |
172 val output = [Pretty.str (Syntax.string_of_term ctxt (prop_of goals))] |
173 val _ = tracing (Syntax.string_of_term ctxt (prop_of goals)) |
173 val _ = tracing (Syntax.string_of_term ctxt (prop_of goals)) |
174 val _ = tracing (Pretty.string_of (Pretty.str (Syntax.string_of_term ctxt (prop_of goals)))) |
174 val _ = tracing (Pretty.string_of (Pretty.str (Syntax.string_of_term ctxt (prop_of goals)))) |
175 in |
175 in |