src/Pure/pattern.ML
changeset 22678 23963361278c
parent 22255 8fcd11cb9be7
child 23222 daca4731942f
     1.1 --- a/src/Pure/pattern.ML	Sat Apr 14 17:36:03 2007 +0200
     1.2 +++ b/src/Pure/pattern.ML	Sat Apr 14 17:36:05 2007 +0200
     1.3 @@ -71,7 +71,7 @@
     1.4  
     1.5  fun proj_fail thy (env,binders,F,_,is,t) =
     1.6    if !trace_unify_fail
     1.7 -  then let val f = Syntax.string_of_vname F
     1.8 +  then let val f = Term.string_of_vname F
     1.9             val xs = bnames binders is
    1.10             val u = string_of_term thy env binders t
    1.11             val ys = bnames binders (subtract (op =) is (loose_bnos t))
    1.12 @@ -83,7 +83,7 @@
    1.13  
    1.14  fun ocheck_fail thy (F,t,binders,env) =
    1.15    if !trace_unify_fail
    1.16 -  then let val f = Syntax.string_of_vname F
    1.17 +  then let val f = Term.string_of_vname F
    1.18             val u = string_of_term thy env binders t
    1.19         in tracing("Variable " ^ f ^ " occurs in term\n" ^ u ^
    1.20                    "\nCannot unify!\n")