repaired whitespace accident from 2505cabfc515
authorhaftmann
Tue Jan 02 23:04:15 2018 +0100 (18 months ago)
changeset 67331a8770603a269
parent 67330 2505cabfc515
child 67332 cb96edae56ef
repaired whitespace accident from 2505cabfc515
src/Pure/thm.ML
     1.1 --- a/src/Pure/thm.ML	Mon Jan 01 20:42:08 2018 +0000
     1.2 +++ b/src/Pure/thm.ML	Tue Jan 02 23:04:15 2018 +0100
     1.3 @@ -1803,10 +1803,10 @@
     1.4    map #1 (Name_Space.markup_table verbose ctxt (Oracles.get (Proof_Context.theory_of ctxt)));
     1.5  
     1.6  fun add_oracle (b, oracle) thy =
     1.7 -    let
     1.8 -      val (name, tab') = Name_Space.define (Context.Theory thy) true (b, ()) (Oracles.get thy);
     1.9 -      val thy' = Oracles.put tab' thy;
    1.10 -    in ((name, invoke_oracle thy' name oracle), thy') end;
    1.11 +  let
    1.12 +    val (name, tab') = Name_Space.define (Context.Theory thy) true (b, ()) (Oracles.get thy);
    1.13 +    val thy' = Oracles.put tab' thy;
    1.14 +  in ((name, invoke_oracle thy' name oracle), thy') end;
    1.15  
    1.16  end;
    1.17