changeset 6085 | 3d8dcb09dbfb |
parent 2672 | 85d7e800d754 |
--- a/src/Pure/deriv.ML Tue Jan 12 12:29:24 1999 +0100 +++ b/src/Pure/deriv.ML Tue Jan 12 12:29:50 1999 +0100 @@ -13,7 +13,7 @@ | Asm of int | Res of deriv | Equal of deriv - | Thm of string + | Thm of string * tag list | Other of deriv; val size : deriv -> int @@ -49,7 +49,7 @@ | Asm of int | Res of deriv | Equal of deriv - | Thm of string + | Thm of string * tag list | Other of deriv; (*At position i, splice in value x, removing ngoal elements*)