| changeset 39557 | fe5722fce758 |
| parent 38838 | 62f6ba39b3d4 |
| child 42287 | d98eb048a2e4 |
--- a/src/HOL/Statespace/DistinctTreeProver.thy Mon Sep 20 15:29:53 2010 +0200 +++ b/src/HOL/Statespace/DistinctTreeProver.thy Mon Sep 20 16:05:25 2010 +0200 @@ -671,7 +671,7 @@ setup {* Theory.add_consts_i const_decls -#> (fn thy => let val ([thm],thy') = PureThy.add_axioms [(("dist_axiom",dist),[])] thy +#> (fn thy => let val ([thm],thy') = Global_Theory.add_axioms [(("dist_axiom",dist),[])] thy in (da := thm; thy') end) *}