src/Pure/context.ML
 changeset 24184 19cb051154fd parent 24141 73baca986087 child 24369 0cb1f4d76452
```     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 =
```