update_name: more uniform treatment of type constraints (NB: type equality is hard to establish in parse trees);
--- a/src/Pure/Syntax/syn_trans.ML Wed Mar 23 21:07:05 2011 +0100
+++ b/src/Pure/Syntax/syn_trans.ML Thu Mar 24 11:45:39 2011 +0100
@@ -198,7 +198,8 @@
if Type_Ext.is_position ty then list_comb (c $ update_name_tr [t] $ ty, ts)
else
list_comb (c $ update_name_tr [t] $
- (Lexicon.fun_type $ (Lexicon.fun_type $ ty $ ty) $ Lexicon.dummy_type), ts)
+ (Lexicon.fun_type $
+ (Lexicon.fun_type $ Lexicon.dummy_type $ ty) $ Lexicon.dummy_type), ts)
| update_name_tr ts = raise TERM ("update_name_tr", ts);
@@ -461,16 +462,25 @@
(* corresponding updates *)
+local
+
+fun upd_type (Type ("fun", [Type ("fun", [_, T]), _])) = T
+ | upd_type _ = dummyT;
+
fun upd_tr' (x_upd, T) =
(case try (unsuffix "_update") x_upd of
- SOME x => (x, if T = dummyT then T else Term.domain_type T)
+ SOME x => (x, upd_type T)
| NONE => raise Match);
+in
+
fun update_name_tr' (Free x) = Free (upd_tr' x)
| update_name_tr' ((c as Const ("_free", _)) $ Free x) = c $ Free (upd_tr' x)
| update_name_tr' (Const x) = Const (upd_tr' x)
| update_name_tr' _ = raise Match;
+end;
+
(* indexed syntax *)