src/Pure/proofterm.ML
changeset 44334 605381e7c7c5
parent 44333 cc53ce50f738
child 45156 a9b6c2ea7bec
     1.1 --- a/src/Pure/proofterm.ML	Sat Aug 20 19:21:03 2011 +0200
     1.2 +++ b/src/Pure/proofterm.ML	Sat Aug 20 20:00:55 2011 +0200
     1.3 @@ -46,8 +46,8 @@
     1.4  
     1.5    val oracle_ord: oracle * oracle -> order
     1.6    val thm_ord: pthm * pthm -> order
     1.7 -  val merge_oracles: oracle Ord_List.T -> oracle Ord_List.T -> oracle Ord_List.T
     1.8 -  val merge_thms: pthm Ord_List.T -> pthm Ord_List.T -> pthm Ord_List.T
     1.9 +  val unions_oracles: oracle Ord_List.T list -> oracle Ord_List.T
    1.10 +  val unions_thms: pthm Ord_List.T list -> pthm Ord_List.T
    1.11    val all_oracles_of: proof_body -> oracle Ord_List.T
    1.12    val approximate_proof_body: proof -> proof_body
    1.13  
    1.14 @@ -237,8 +237,8 @@
    1.15  val oracle_ord = prod_ord fast_string_ord Term_Ord.fast_term_ord;
    1.16  fun thm_ord ((i, _): pthm, (j, _)) = int_ord (j, i);
    1.17  
    1.18 -val merge_oracles = Ord_List.union oracle_ord;
    1.19 -val merge_thms = Ord_List.union thm_ord;
    1.20 +val unions_oracles = Ord_List.unions oracle_ord;
    1.21 +val unions_thms = Ord_List.unions thm_ord;
    1.22  
    1.23  val all_oracles_of =
    1.24    let
    1.25 @@ -249,8 +249,8 @@
    1.26            let
    1.27              val body' = Future.join body;
    1.28              val (x', seen') = collect body' (x, Inttab.update (i, ()) seen);
    1.29 -          in (merge_oracles oracles x', seen') end);
    1.30 -  in fn body => #1 (collect body ([], Inttab.empty)) end;
    1.31 +          in (if null oracles then x' else oracles :: x', seen') end);
    1.32 +  in fn body => unions_oracles (#1 (collect body ([], Inttab.empty))) end;
    1.33  
    1.34  fun approximate_proof_body prf =
    1.35    let
    1.36 @@ -1385,8 +1385,11 @@
    1.37  fun fulfill_norm_proof thy ps body0 =
    1.38    let
    1.39      val PBody {oracles = oracles0, thms = thms0, proof = proof0} = body0;
    1.40 -    val oracles = fold (fn (_, PBody {oracles, ...}) => merge_oracles oracles) ps oracles0;
    1.41 -    val thms = fold (fn (_, PBody {thms, ...}) => merge_thms thms) ps thms0;
    1.42 +    val oracles =
    1.43 +      unions_oracles
    1.44 +        (fold (fn (_, PBody {oracles, ...}) => not (null oracles) ? cons oracles) ps [oracles0]);
    1.45 +    val thms =
    1.46 +      unions_thms (fold (fn (_, PBody {thms, ...}) => not (null thms) ? cons thms) ps [thms0]);
    1.47      val proofs = fold (fn (i, PBody {proof, ...}) => Inttab.update (i, proof)) ps Inttab.empty;
    1.48  
    1.49      fun fill (Promise (i, prop, Ts)) =