src/Pure/Syntax/syntax_trans.ML
changeset 55948 bb21b380f65d
parent 52177 15fcad6eb956
child 56243 2e10a36b8d46
--- 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;