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