src/Pure/context.ML
changeset 32784 1a5dde5079ac
parent 32738 15bb09ca0378
child 33031 b75c35574e04
     1.1 --- a/src/Pure/context.ML	Wed Sep 30 19:04:48 2009 +0200
     1.2 +++ b/src/Pure/context.ML	Wed Sep 30 22:20:58 2009 +0200
     1.3 @@ -455,7 +455,7 @@
     1.4  
     1.5  fun init_proof thy = Prf (init_data thy, check_thy thy);
     1.6  
     1.7 -fun transfer_proof thy' (prf as Prf (data, thy_ref)) =
     1.8 +fun transfer_proof thy' (Prf (data, thy_ref)) =
     1.9    let
    1.10      val thy = deref thy_ref;
    1.11      val _ = subthy (thy, thy') orelse error "transfer proof context: not a super theory";