# HG changeset patch
# User wenzelm
# Date 1248016114 -7200
# Node ID 371aacbbd6efef2637edb0c1df9711bf19612e03
# Parent  f4b74cbecdafe5c59586a5b8bcf4660e1ae61f28
tuned;

diff -r f4b74cbecdaf -r 371aacbbd6ef src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Sun Jul 19 14:15:47 2009 +0200
+++ b/src/Pure/proofterm.ML	Sun Jul 19 17:08:34 2009 +0200
@@ -207,7 +207,8 @@
                     in ((oracle, true, failed), seen') end)
               end);
       in ((oracle orelse not (null oracles), unfinished, failed), seen) end;
-    val (oracle, unfinished, failed) = #1 (fold status bodies ((false, false, false), Inttab.empty));
+    val (oracle, unfinished, failed) =
+      #1 (fold status bodies ((false, false, false), Inttab.empty));
   in {oracle = oracle, unfinished = unfinished, failed = failed} end;
 
 
@@ -221,13 +222,14 @@
 
 val all_oracles_of =
   let
-    fun collect (PBody {oracles, thms, ...}) = thms |> fold (fn (i, (_, _, body)) => fn (x, seen) =>
-      if Inttab.defined seen i then (x, seen)
-      else
-        let
-          val body' = Future.join body;
-          val (x', seen') = collect body' (x, Inttab.update (i, ()) seen);
-        in (merge_oracles oracles x', seen') end);
+    fun collect (PBody {oracles, thms, ...}) =
+      thms |> fold (fn (i, (_, _, body)) => fn (x, seen) =>
+        if Inttab.defined seen i then (x, seen)
+        else
+          let
+            val body' = Future.join body;
+            val (x', seen') = collect body' (x, Inttab.update (i, ()) seen);
+          in (merge_oracles oracles x', seen') end);
   in fn body => #1 (collect body ([], Inttab.empty)) end;
 
 fun approximate_proof_body prf =
@@ -292,7 +294,8 @@
       | proof (OfClass (T, c)) = OfClass (typ T, c)
       | proof (Oracle (a, prop, SOME Ts)) = Oracle (a, prop, SOME (typs Ts))
       | proof (Promise (i, prop, Ts)) = Promise (i, prop, typs Ts)
-      | proof (PThm (i, ((a, prop, SOME Ts), body))) = PThm (i, ((a, prop, SOME (typs Ts)), body))
+      | proof (PThm (i, ((a, prop, SOME Ts), body))) =
+          PThm (i, ((a, prop, SOME (typs Ts)), body))
       | proof _ = raise Same.SAME;
   in Same.commit proof end;
 
@@ -332,7 +335,8 @@
   | change_type (SOME [T]) (OfClass (_, c)) = OfClass (T, c)
   | change_type opTs (Oracle (name, prop, _)) = Oracle (name, prop, opTs)
   | change_type opTs (Promise _) = error "change_type: unexpected promise"
-  | change_type opTs (PThm (i, ((name, prop, _), body))) = PThm (i, ((name, prop, opTs), body))
+  | change_type opTs (PThm (i, ((name, prop, _), body))) =
+      PThm (i, ((name, prop, opTs), body))
   | change_type _ prf = prf;
 
 
@@ -513,7 +517,8 @@
       | subst' _ _ = raise Same.SAME
     and substh' lev t = (subst' lev t handle Same.SAME => t);
 
-    fun subst lev (AbsP (a, t, body)) = (AbsP (a, Same.map_option (subst' lev) t, substh lev body)
+    fun subst lev (AbsP (a, t, body)) =
+        (AbsP (a, Same.map_option (subst' lev) t, substh lev body)
           handle Same.SAME => AbsP (a, t, subst lev body))
       | subst lev (Abst (a, T, body)) = Abst (a, T, subst (lev+1) body)
       | subst lev (prf %% prf') = (subst lev prf %% substh lev prf'