# HG changeset patch
# User wenzelm
# Date 1300806950 -3600
# Node ID 006095137a81eafca0c2ebe34ad43bf6afe99fc0
# Parent  34f1d2d812843493eab3282653f38b586417c181
update_name_tr: more precise handling of explicit constraints, including positions;

diff -r 34f1d2d81284 -r 006095137a81 src/HOL/Isar_Examples/Hoare.thy
--- a/src/HOL/Isar_Examples/Hoare.thy	Tue Mar 22 15:32:47 2011 +0100
+++ b/src/HOL/Isar_Examples/Hoare.thy	Tue Mar 22 16:15:50 2011 +0100
@@ -302,7 +302,7 @@
   then show ?thesis by simp
 qed
 
-lemma assign: "|- P [\<acute>a/\<acute>x] \<acute>x := \<acute>a P"
+lemma assign: "|- P [\<acute>a/\<acute>x::'a] \<acute>x := \<acute>a P"
   by (rule basic)
 
 text {* Note that above formulation of assignment corresponds to our
diff -r 34f1d2d81284 -r 006095137a81 src/Pure/Syntax/lexicon.ML
--- a/src/Pure/Syntax/lexicon.ML	Tue Mar 22 15:32:47 2011 +0100
+++ b/src/Pure/Syntax/lexicon.ML	Tue Mar 22 16:15:50 2011 +0100
@@ -42,6 +42,8 @@
     case_fixed: string -> 'a,
     case_default: string -> 'a} -> string -> 'a
   val is_marked: string -> bool
+  val dummy_type: term
+  val fun_type: term
   val pretty_position: Position.T -> Pretty.T
   val encode_position: Position.T -> string
   val decode_position: string -> Position.T option
@@ -380,6 +382,9 @@
   unmark {case_class = K true, case_type = K true, case_const = K true,
     case_fixed = K true, case_default = K false};
 
+val dummy_type = const (mark_type "dummy");
+val fun_type = const (mark_type "fun");
+
 
 (* read numbers *)
 
diff -r 34f1d2d81284 -r 006095137a81 src/Pure/Syntax/syn_trans.ML
--- a/src/Pure/Syntax/syn_trans.ML	Tue Mar 22 15:32:47 2011 +0100
+++ b/src/Pure/Syntax/syn_trans.ML	Tue Mar 22 16:15:50 2011 +0100
@@ -188,8 +188,10 @@
 fun update_name_tr (Free (x, T) :: ts) = list_comb (Free (suffix "_update" x, T), ts)
   | update_name_tr (Const (x, T) :: ts) = list_comb (Const (suffix "_update" x, T), ts)
   | update_name_tr (((c as Const ("_constrain", _)) $ t $ ty) :: ts) =
-      list_comb (c $ update_name_tr [t] $
-        (Lexicon.const "\\<^type>fun" $ ty $ Lexicon.const "\\<^type>dummy"), ts)
+      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)
   | update_name_tr ts = raise TERM ("update_name_tr", ts);
 
 
diff -r 34f1d2d81284 -r 006095137a81 src/Pure/Syntax/type_ext.ML
--- a/src/Pure/Syntax/type_ext.ML	Tue Mar 22 15:32:47 2011 +0100
+++ b/src/Pure/Syntax/type_ext.ML	Tue Mar 22 16:15:50 2011 +0100
@@ -9,6 +9,7 @@
   val sort_of_term: term -> sort
   val term_sorts: term -> (indexname * sort) list
   val typ_of_term: (indexname -> sort) -> term -> typ
+  val is_position: term -> bool
   val strip_positions: term -> term
   val strip_positions_ast: Ast.ast -> Ast.ast
   val decode_term: (((string * int) * sort) list -> string * int -> sort) ->