equal
deleted
inserted
replaced
72 fun proj_fail thy (env,binders,F,_,is,t) = |
72 fun proj_fail thy (env,binders,F,_,is,t) = |
73 if !trace_unify_fail |
73 if !trace_unify_fail |
74 then let val f = Syntax.string_of_vname F |
74 then let val f = Syntax.string_of_vname F |
75 val xs = bnames binders is |
75 val xs = bnames binders is |
76 val u = string_of_term thy env binders t |
76 val u = string_of_term thy env binders t |
77 val ys = bnames binders (loose_bnos t \\ is) |
77 val ys = bnames binders (subtract (op =) is (loose_bnos t)) |
78 in tracing("Cannot unify variable " ^ f ^ |
78 in tracing("Cannot unify variable " ^ f ^ |
79 " (depending on bound variables " ^ xs ^ ")\nwith term " ^ u ^ |
79 " (depending on bound variables " ^ xs ^ ")\nwith term " ^ u ^ |
80 "\nTerm contains additional bound variable(s) " ^ ys) |
80 "\nTerm contains additional bound variable(s) " ^ ys) |
81 end |
81 end |
82 else () |
82 else () |