src/Pure/pattern.ML
changeset 26939 1035c89b4c02
parent 26831 6c3eec8157d3
child 28348 4f2406ddd9ea
     1.1 --- a/src/Pure/pattern.ML	Sat May 17 23:53:20 2008 +0200
     1.2 +++ b/src/Pure/pattern.ML	Sun May 18 15:04:09 2008 +0200
     1.3 @@ -41,16 +41,17 @@
     1.4  
     1.5  val trace_unify_fail = ref false;
     1.6  
     1.7 -fun string_of_term thy env binders t = Sign.string_of_term thy
     1.8 -  (Envir.norm_term env (subst_bounds(map Free binders,t)));
     1.9 +fun string_of_term thy env binders t =
    1.10 +  Syntax.string_of_term_global thy
    1.11 +    (Envir.norm_term env (subst_bounds (map Free binders, t)));
    1.12  
    1.13  fun bname binders i = fst (nth binders i);
    1.14  fun bnames binders is = space_implode " " (map (bname binders) is);
    1.15  
    1.16  fun typ_clash thy (tye,T,U) =
    1.17    if !trace_unify_fail
    1.18 -  then let val t = Sign.string_of_typ thy (Envir.norm_type tye T)
    1.19 -           and u = Sign.string_of_typ thy (Envir.norm_type tye U)
    1.20 +  then let val t = Syntax.string_of_typ_global thy (Envir.norm_type tye T)
    1.21 +           and u = Syntax.string_of_typ_global thy (Envir.norm_type tye U)
    1.22         in tracing("The following types do not unify:\n" ^ t ^ "\n" ^ u) end
    1.23    else ()
    1.24