| changeset 191 | fe5d88d4c7e1 |
| parent 69 | e7588b53d6b0 |
| child 214 | ed6a3e2b1a33 |
--- a/src/Pure/tactic.ML Thu Dec 09 11:39:33 1993 +0100 +++ b/src/Pure/tactic.ML Fri Dec 10 10:36:39 1993 +0100 @@ -206,7 +206,7 @@ compose_tac (bires_flg, lift_inst_rule (state, i, sinsts, rule), nsubgoal) i handle TERM (msg,_) => (writeln msg; no_tac) - | THM _ => no_tac ); + | THM (msg,_,_) => (writeln msg; no_tac) ); (*Resolve version*) fun res_inst_tac sinsts rule i =