thread-safeness: when creating certified items, perform Theory.check_thy *last*;
authorwenzelm
Wed Aug 08 16:40:20 2007 +0200 (2007-08-08)
changeset 2418419cb051154fd
parent 24183 a46b758941a4
child 24185 cb0c4bd149a6
thread-safeness: when creating certified items, perform Theory.check_thy *last*;
tuned datatype proof;
src/Pure/context.ML
     1.1 --- a/src/Pure/context.ML	Wed Aug 08 14:00:09 2007 +0200
     1.2 +++ b/src/Pure/context.ML	Wed Aug 08 16:40:20 2007 +0200
     1.3 @@ -415,11 +415,11 @@
     1.4  
     1.5  (* datatype proof *)
     1.6  
     1.7 -datatype proof = Proof of theory_ref * Object.T Datatab.table;
     1.8 +datatype proof = Prf of Object.T Datatab.table * theory_ref;
     1.9  
    1.10 -fun theory_of_proof (Proof (thy_ref, _)) = deref thy_ref;
    1.11 -fun data_of_proof (Proof (_, data)) = data;
    1.12 -fun map_prf f (Proof (thy_ref, data)) = Proof (thy_ref, f data);
    1.13 +fun theory_of_proof (Prf (_, thy_ref)) = deref thy_ref;
    1.14 +fun data_of_proof (Prf (data, _)) = data;
    1.15 +fun map_prf f (Prf (data, thy_ref)) = Prf (f data, thy_ref);
    1.16  
    1.17  
    1.18  (* proof data kinds *)
    1.19 @@ -441,15 +441,16 @@
    1.20  
    1.21  in
    1.22  
    1.23 -fun init_proof thy = Proof (check_thy thy, init_data thy);
    1.24 +fun init_proof thy = Prf (init_data thy, check_thy thy);
    1.25  
    1.26 -fun transfer_proof thy' (prf as Proof (thy_ref, data)) =
    1.27 +fun transfer_proof thy' (prf as Prf (data, thy_ref)) =
    1.28    let
    1.29      val thy = deref thy_ref;
    1.30      val _ = subthy (thy, thy') orelse error "transfer proof context: not a super theory";
    1.31      val _ = check_thy thy;
    1.32 +    val data' = init_new_data data thy';
    1.33      val thy_ref' = check_thy thy';
    1.34 -  in Proof (thy_ref', init_new_data data thy') end;
    1.35 +  in Prf (data', thy_ref') end;
    1.36  
    1.37  
    1.38  structure ProofData =