src/Pure/thm.ML
changeset 1566 a203d206fab7
parent 1539 f21c8fab7c3c
child 1569 a89f246dee0e
equal deleted inserted replaced
1565:70dd38777109 1566:a203d206fab7
   540     (Symtab.dest (#new_axioms (rep_theory thy)));
   540     (Symtab.dest (#new_axioms (rep_theory thy)));
   541 
   541 
   542 fun name_thm (thy, name, th as Thm {sign, der, maxidx, shyps, hyps, prop}) = 
   542 fun name_thm (thy, name, th as Thm {sign, der, maxidx, shyps, hyps, prop}) = 
   543     if Sign.eq_sg (sign, sign_of thy) then
   543     if Sign.eq_sg (sign, sign_of thy) then
   544 	Thm {sign = sign, 
   544 	Thm {sign = sign, 
   545 	     der = Infer (Theorem(thy,name), []),	
   545 	     der = Infer (Theorem(thy,name), [der]),
   546 	     maxidx = maxidx,
   546 	     maxidx = maxidx,
   547 	     shyps = shyps, 
   547 	     shyps = shyps, 
   548 	     hyps = hyps, 
   548 	     hyps = hyps, 
   549 	     prop = prop}
   549 	     prop = prop}
   550     else raise THM ("name_thm", 0, [th]);
   550     else raise THM ("name_thm", 0, [th]);