src/Provers/classical.ML
changeset 32863 5e8cef567042
parent 32862 1fc86cec3bdf
child 32952 aeb1e44fbc19
     1.1 --- a/src/Provers/classical.ML	Fri Oct 02 22:15:30 2009 +0200
     1.2 +++ b/src/Provers/classical.ML	Fri Oct 02 23:15:36 2009 +0200
     1.3 @@ -768,7 +768,7 @@
     1.4  (*Non-deterministic!  Could always expand the first unsafe connective.
     1.5    That's hard to implement and did not perform better in experiments, due to
     1.6    greater search depth required.*)
     1.7 -fun dup_step_tac (cs as (CS{dup_netpair,...})) =
     1.8 +fun dup_step_tac (CS {dup_netpair, ...}) =
     1.9    biresolve_from_nets_tac dup_netpair;
    1.10  
    1.11  (*Searching to depth m. A variant called nodup_depth_tac appears in clasimp.ML*)