equal
deleted
inserted
replaced
8 |
8 |
9 (* FIXME: |
9 (* FIXME: |
10 fun refute_action args timeout {pre=st, ...} = |
10 fun refute_action args timeout {pre=st, ...} = |
11 let |
11 let |
12 val subgoal = 1 |
12 val subgoal = 1 |
13 val thy = Proof.theory_of st |
13 val thy = Proof.theory_of st |
14 val thm = goal_thm_of st |
14 val thm = #goal (Proof.raw_goal st) |
15 |
15 |
16 val refute = Refute.refute_goal thy args thm |
16 val refute = Refute.refute_goal thy args thm |
17 val _ = TimeLimit.timeLimit timeout refute subgoal |
17 val _ = TimeLimit.timeLimit timeout refute subgoal |
18 in |
18 in |
19 val writ_log = Substring.full (the (Symtab.lookup tab "writeln")) |
19 val writ_log = Substring.full (the (Symtab.lookup tab "writeln")) |