--- a/src/Pure/Syntax/syntax_trans.ML Thu Mar 06 10:11:38 2014 +0100
+++ b/src/Pure/Syntax/syntax_trans.ML Thu Mar 06 10:12:47 2014 +0100
@@ -124,7 +124,7 @@
| lambda_ast_tr asts = raise Ast.AST ("lambda_ast_tr", asts);
fun absfree_proper (x, T) t =
- if can Name.dest_internal x
+ if Name.is_internal x
then error ("Illegal internal variable in abstraction: " ^ quote x)
else absfree (x, T) t;
@@ -316,7 +316,7 @@
val body = body_of tm;
val rev_new_vars = Term.rename_wrt_term body vars;
fun subst (x, T) b =
- if can Name.dest_internal x andalso not (Term.is_dependent b)
+ if Name.is_internal x andalso not (Term.is_dependent b)
then (Const ("_idtdummy", T), incr_boundvars ~1 b)
else (mark_bound_abs (x, T), Term.subst_bound (mark_bound_body (x, T), b));
val (rev_vars', body') = fold_map subst rev_new_vars body;