author | wenzelm |
Thu, 02 Jun 2005 09:11:34 +0200 | |
changeset 16180 | a51be5cbd81d |
parent 16179 | fa7e70be26b0 |
child 16181 | 22324687e2d2 |
--- a/src/Pure/axclass.ML Thu Jun 02 09:11:32 2005 +0200 +++ b/src/Pure/axclass.ML Thu Jun 02 09:11:34 2005 +0200 @@ -230,7 +230,7 @@ val final_thy = axms_thy |> (#1 o PureThy.add_thms ((map #1 axms ~~ axioms) ~~ atts)) - |> Theory.parent_path + |> Theory.restore_naming class_thy |> (#1 o PureThy.add_thms [Thm.no_attributes (intro_name bclass, intro)]) |> put_axclass_info class info; in (final_thy, {intro = intro, axioms = axioms}) end;