diff -r 1fc86cec3bdf -r 5e8cef567042 src/Provers/classical.ML --- a/src/Provers/classical.ML Fri Oct 02 22:15:30 2009 +0200 +++ b/src/Provers/classical.ML Fri Oct 02 23:15:36 2009 +0200 @@ -768,7 +768,7 @@ (*Non-deterministic! Could always expand the first unsafe connective. That's hard to implement and did not perform better in experiments, due to greater search depth required.*) -fun dup_step_tac (cs as (CS{dup_netpair,...})) = +fun dup_step_tac (CS {dup_netpair, ...}) = biresolve_from_nets_tac dup_netpair; (*Searching to depth m. A variant called nodup_depth_tac appears in clasimp.ML*)