--- a/src/Pure/thm.ML Mon Jan 01 20:42:08 2018 +0000
+++ b/src/Pure/thm.ML Tue Jan 02 23:04:15 2018 +0100
@@ -1803,10 +1803,10 @@
map #1 (Name_Space.markup_table verbose ctxt (Oracles.get (Proof_Context.theory_of ctxt)));
fun add_oracle (b, oracle) thy =
- let
- val (name, tab') = Name_Space.define (Context.Theory thy) true (b, ()) (Oracles.get thy);
- val thy' = Oracles.put tab' thy;
- in ((name, invoke_oracle thy' name oracle), thy') end;
+ let
+ val (name, tab') = Name_Space.define (Context.Theory thy) true (b, ()) (Oracles.get thy);
+ val thy' = Oracles.put tab' thy;
+ in ((name, invoke_oracle thy' name oracle), thy') end;
end;