src/Pure/Tools/compute.ML

       invoke_oracle_i thy "Pure.compute" (thy, Param (r, n, ct))
     end
 
 fun rewrite r ct = rewrite_param r default_naming ct
 
-(* setup of the Pure.compute oracle *)
+
+(* theory setup *)
+
 fun compute_oracle (thy, Param (r, naming, ct)) =
     let
         val _ = Theory.assert_super (theory_of r) thy
         val t' = compute r naming ct
     in
         Logic.mk_equals (term_of ct, t')
     end
 
-val _ = Context.add_setup [Theory.add_oracle ("compute", compute_oracle)]
+val _ = Context.add_setup (Theory.add_oracle ("compute", compute_oracle))
 
 end