# HG changeset patch
# User wenzelm
# Date 1211115881 -7200
# Node ID efe3e0e235d63150546efca62f01c5ae06d86c18
# Parent  133905a0c493cbeaaf779ca098948fd02afd9c9c
Syntax.string_of_typ: proper context;

diff -r 133905a0c493 -r efe3e0e235d6 src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Sun May 18 15:04:37 2008 +0200
+++ b/src/Pure/Isar/locale.ML	Sun May 18 15:04:41 2008 +0200
@@ -683,7 +683,7 @@
         let
           val T' = Envir.norm_type (fst envir) T;
           val U' = Envir.norm_type (fst envir) U;
-          val prt = Sign.string_of_typ thy;
+          val prt = Syntax.string_of_typ ctxt;
         in
           raise TYPE ("unify_parms: failed to unify types " ^
             prt U' ^ " and " ^ prt T', [U', T'], [])