changeset 6966 | cfa87aef9ccd |
parent 6113 | b321f5aaa5f4 |
child 7355 | 4c43090659ca |
--- a/src/FOL/IFOL.ML Sat Jul 10 21:43:27 1999 +0200 +++ b/src/FOL/IFOL.ML Sat Jul 10 21:44:26 1999 +0200 @@ -248,7 +248,7 @@ (*Apply an equality or definition ONCE. Fails unless the substitution has an effect*) fun stac th = - let val th' = th RS meta_eq_to_obj_eq handle _ => th + let val th' = th RS meta_eq_to_obj_eq handle THM _ => th in CHANGED_GOAL (rtac (th' RS ssubst)) end;