changeset 1566 | a203d206fab7 |
parent 1539 | f21c8fab7c3c |
child 1569 | a89f246dee0e |
--- a/src/Pure/thm.ML Mon Mar 11 14:13:36 1996 +0100 +++ b/src/Pure/thm.ML Mon Mar 11 14:16:35 1996 +0100 @@ -542,7 +542,7 @@ fun name_thm (thy, name, th as Thm {sign, der, maxidx, shyps, hyps, prop}) = if Sign.eq_sg (sign, sign_of thy) then Thm {sign = sign, - der = Infer (Theorem(thy,name), []), + der = Infer (Theorem(thy,name), [der]), maxidx = maxidx, shyps = shyps, hyps = hyps,