| changeset 33095 | bbd52d2f8696 |
| parent 32958 | 3228627994d9 |
| child 33277 | 1bdc3c732fdd |
--- a/src/Pure/drule.ML Sat Oct 24 19:24:50 2009 +0200 +++ b/src/Pure/drule.ML Sat Oct 24 19:47:37 2009 +0200 @@ -452,7 +452,7 @@ val read_prop = certify o SimpleSyntax.read_prop; -fun get_def thy = Thm.axiom thy o NameSpace.intern (Theory.axiom_space thy) o Thm.def_name; +fun get_def thy = Thm.axiom thy o Name_Space.intern (Theory.axiom_space thy) o Thm.def_name; fun store_thm name th = Context.>>> (Context.map_theory_result (PureThy.store_thm (Binding.name name, th)));