diff options
Diffstat (limited to 'proofs/signatures/th_quant.plf')
-rwxr-xr-x | proofs/signatures/th_quant.plf | 5 |
1 files changed, 1 insertions, 4 deletions
diff --git a/proofs/signatures/th_quant.plf b/proofs/signatures/th_quant.plf index d85b2115c..e212f835d 100755 --- a/proofs/signatures/th_quant.plf +++ b/proofs/signatures/th_quant.plf @@ -14,10 +14,7 @@ (match ti ((apply si1 si2 ti1 ti2) (match (is_inst_t ti1 t1 k) (tt (is_inst_t ti2 t2 k)) (ff ff))) (default ff))) - (default - (match ti - ((apply si1 si2 ti1 ti2) ff) - (default (eqterm ti (ifmarked t k t))))))) + (default (eqterm ti (ifmarked t k t))))) (program is_inst_f ((fi formula) (f formula) (k term)) bool (match f |