src/HOL/Statespace/DistinctTreeProver.thy
changeset 27691 ce171cbd4b93
parent 25364 7f012f56efa3
child 28819 daca685d7bb7
     1.1 --- a/src/HOL/Statespace/DistinctTreeProver.thy	Tue Jul 29 08:15:39 2008 +0200
     1.2 +++ b/src/HOL/Statespace/DistinctTreeProver.thy	Tue Jul 29 08:15:40 2008 +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_i [(("dist_axiom",dist),[])] thy
     1.8 +#> (fn thy  => let val ([thm],thy') = PureThy.add_axioms [(("dist_axiom",dist),[])] thy
     1.9                 in (da := thm; thy') end)
    1.10  *}
    1.11