# 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'