Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
name_thm: now keeps the previous deriviation!
authorpaulson
Mon, 11 Mar 1996 14:16:35 +0100
changeset 1566 a203d206fab7
parent 1565 70dd38777109
child 1567 02bbdc811ae7
name_thm: now keeps the previous deriviation!
src/Pure/thm.ML file | annotate | diff | comparison | revisions 
--- 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,
isabelle