# HG changeset patch # User wenzelm # Date 1300963539 -3600 # Node ID 58b465952287fa2512ae575976ef0fe9cd073b8e # Parent 71662f36b57306c32b401b314090ecef3aac0ad8 update_name: more uniform treatment of type constraints (NB: type equality is hard to establish in parse trees); diff -r 71662f36b573 -r 58b465952287 src/Pure/Syntax/syn_trans.ML --- 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 *)