# HG changeset patch
# User haftmann
# Date 1514930655 -3600
# Node ID a8770603a269c83c1efac0736d2cd0a9522f1e77
# Parent  2505cabfc515c46184305c28aca694635e8fb4ba
repaired whitespace accident from 2505cabfc515

diff -r 2505cabfc515 -r a8770603a269 src/Pure/thm.ML
--- 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;