| changeset 33095 | bbd52d2f8696 |
| parent 32786 | f1ac4b515af9 |
| child 33167 | f02b804305d6 |
--- a/src/Pure/pure_thy.ML Sat Oct 24 19:24:50 2009 +0200 +++ b/src/Pure/pure_thy.ML Sat Oct 24 19:47:37 2009 +0200 @@ -146,7 +146,7 @@ else let val naming = Sign.naming_of thy; - val name = NameSpace.full_name naming b; + val name = Name_Space.full_name naming b; val (thy', thms') = register_proofs (apsnd (post_name name) (app_att (thy, pre_name name thms))); val thms'' = map (Thm.transfer thy') thms';