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