src/Pure/type_infer.ML
changeset 42360 da8817d01e7c
parent 42284 326f57825e1a
child 42383 0ae4ad40d7b5
     1.1 --- a/src/Pure/type_infer.ML	Sat Apr 16 15:25:25 2011 +0200
     1.2 +++ b/src/Pure/type_infer.ML	Sat Apr 16 15:47:52 2011 +0200
     1.3 @@ -219,7 +219,7 @@
     1.4  
     1.5  fun unify ctxt pp =
     1.6    let
     1.7 -    val thy = ProofContext.theory_of ctxt;
     1.8 +    val thy = Proof_Context.theory_of ctxt;
     1.9      val arity_sorts = Type.arity_sorts pp (Sign.tsig_of thy);
    1.10  
    1.11