# 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 *)