src/Pure/Tools/compute.ML
changeset 18708 4b3dadb4fe33
parent 17795 5b18c3343028
child 19482 9f11af8f7ef9
     1.1 --- a/src/Pure/Tools/compute.ML	Thu Jan 19 15:45:10 2006 +0100
     1.2 +++ b/src/Pure/Tools/compute.ML	Thu Jan 19 21:22:08 2006 +0100
     1.3 @@ -277,7 +277,9 @@
     1.4  
     1.5  fun rewrite r ct = rewrite_param r default_naming ct
     1.6  
     1.7 -(* setup of the Pure.compute oracle *)
     1.8 +
     1.9 +(* theory setup *)
    1.10 +
    1.11  fun compute_oracle (thy, Param (r, naming, ct)) =
    1.12      let
    1.13          val _ = Theory.assert_super (theory_of r) thy
    1.14 @@ -286,6 +288,6 @@
    1.15          Logic.mk_equals (term_of ct, t')
    1.16      end
    1.17  
    1.18 -val _ = Context.add_setup [Theory.add_oracle ("compute", compute_oracle)]
    1.19 +val _ = Context.add_setup (Theory.add_oracle ("compute", compute_oracle))
    1.20  
    1.21  end