# HG changeset patch
# User wenzelm
# Date 1348935826 -7200
# Node ID de49d9b4d7bc2fdfe53d0b89cf256775eb7487c7
# Parent  251342b60a820950a0e56467f26b44325c29f82f
more explicit Syntax_Trans.mark_bound_abs/mark_bound_body: preserve type information for show_markup;

diff -r 251342b60a82 -r de49d9b4d7bc src/CCL/Term.thy
--- a/src/CCL/Term.thy	Sat Sep 29 16:51:04 2012 +0200
+++ b/src/CCL/Term.thy	Sat Sep 29 18:23:46 2012 +0200
@@ -56,7 +56,7 @@
 (** Quantifier translations: variable binding **)
 
 (* FIXME does not handle "_idtdummy" *)
-(* FIXME should use Syntax_Trans.mark_bound(T), Syntax_Trans.variant_abs' *)
+(* FIXME should use Syntax_Trans.mark_bound, Syntax_Trans.variant_abs' *)
 
 fun let_tr [Free x, a, b] = Const(@{const_syntax let},dummyT) $ a $ absfree x b;
 fun let_tr' [a,Abs(id,T,b)] =
diff -r 251342b60a82 -r de49d9b4d7bc src/HOL/Big_Operators.thy
--- a/src/HOL/Big_Operators.thy	Sat Sep 29 16:51:04 2012 +0200
+++ b/src/HOL/Big_Operators.thy	Sat Sep 29 18:23:46 2012 +0200
@@ -201,10 +201,12 @@
         if x <> y then raise Match
         else
           let
-            val x' = Syntax_Trans.mark_bound x;
+            val x' = Syntax_Trans.mark_bound_body (x, Tx);
             val t' = subst_bound (x', t);
             val P' = subst_bound (x', P);
-          in Syntax.const @{syntax_const "_qsetsum"} $ Syntax_Trans.mark_bound x $ P' $ t' end
+          in
+            Syntax.const @{syntax_const "_qsetsum"} $ Syntax_Trans.mark_bound_abs (x, Tx) $ P' $ t'
+          end
     | setsum_tr' _ = raise Match;
 in [(@{const_syntax setsum}, setsum_tr')] end
 *}
diff -r 251342b60a82 -r de49d9b4d7bc src/HOL/Orderings.thy
--- a/src/HOL/Orderings.thy	Sat Sep 29 16:51:04 2012 +0200
+++ b/src/HOL/Orderings.thy	Sat Sep 29 18:23:46 2012 +0200
@@ -644,16 +644,16 @@
       Const (@{syntax_const "_bound"}, _) $ Free (v', _) => v = v'
     | _ => false);
   fun contains_var v = Term.exists_subterm (fn Free (x, _) => x = v | _ => false);
-  fun mk v c n P = Syntax.const c $ Syntax_Trans.mark_bound v $ n $ P;
+  fun mk x c n P = Syntax.const c $ Syntax_Trans.mark_bound_body x $ n $ P;
 
   fun tr' q = (q,
-    fn [Const (@{syntax_const "_bound"}, _) $ Free (v, _),
+    fn [Const (@{syntax_const "_bound"}, _) $ Free (v, T),
         Const (c, _) $ (Const (d, _) $ t $ u) $ P] =>
         (case AList.lookup (op =) trans (q, c, d) of
           NONE => raise Match
         | SOME (l, g) =>
-            if matches_bound v t andalso not (contains_var v u) then mk v l u P
-            else if matches_bound v u andalso not (contains_var v t) then mk v g t P
+            if matches_bound v t andalso not (contains_var v u) then mk (v, T) l u P
+            else if matches_bound v u andalso not (contains_var v t) then mk (v, T) g t P
             else raise Match)
      | _ => raise Match);
 in [tr' All_binder, tr' Ex_binder] end
diff -r 251342b60a82 -r de49d9b4d7bc src/HOL/Set.thy
--- a/src/HOL/Set.thy	Sat Sep 29 16:51:04 2012 +0200
+++ b/src/HOL/Set.thy	Sat Sep 29 18:23:46 2012 +0200
@@ -270,17 +270,17 @@
     ((Ex_binder, conj, sbset), @{syntax_const "_setlessEx"}),
     ((Ex_binder, conj, sbset_eq), @{syntax_const "_setleEx"})];
 
-  fun mk v v' c n P =
+  fun mk v (v', T) c n P =
     if v = v' andalso not (Term.exists_subterm (fn Free (x, _) => x = v | _ => false) n)
-    then Syntax.const c $ Syntax_Trans.mark_bound v' $ n $ P else raise Match;
+    then Syntax.const c $ Syntax_Trans.mark_bound_body (v', T) $ n $ P else raise Match;
 
   fun tr' q = (q,
         fn [Const (@{syntax_const "_bound"}, _) $ Free (v, Type (@{type_name set}, _)),
             Const (c, _) $
-              (Const (d, _) $ (Const (@{syntax_const "_bound"}, _) $ Free (v', _)) $ n) $ P] =>
+              (Const (d, _) $ (Const (@{syntax_const "_bound"}, _) $ Free (v', T)) $ n) $ P] =>
             (case AList.lookup (op =) trans (q, c, d) of
               NONE => raise Match
-            | SOME l => mk v v' l n P)
+            | SOME l => mk v (v', T) l n P)
          | _ => raise Match);
 in
   [tr' All_binder, tr' Ex_binder]
diff -r 251342b60a82 -r de49d9b4d7bc src/HOL/Tools/Datatype/datatype_case.ML
--- a/src/HOL/Tools/Datatype/datatype_case.ML	Sat Sep 29 16:51:04 2012 +0200
+++ b/src/HOL/Tools/Datatype/datatype_case.ML	Sat Sep 29 18:23:46 2012 +0200
@@ -451,12 +451,12 @@
         let val xs = Term.add_frees pat [] in
           Syntax.const @{syntax_const "_case1"} $
             map_aterms
-              (fn Free p => Syntax_Trans.mark_boundT p
+              (fn Free p => Syntax_Trans.mark_bound_abs p
                 | Const (s, _) => Syntax.const (Lexicon.mark_const s)
                 | t => t) pat $
             map_aterms
-              (fn x as Free (s, T) =>
-                  if member (op =) xs (s, T) then Syntax_Trans.mark_bound s else x
+              (fn x as Free v =>
+                  if member (op =) xs v then Syntax_Trans.mark_bound_body v else x
                 | t => t) rhs
         end;
     in
diff -r 251342b60a82 -r de49d9b4d7bc src/Pure/Isar/obtain.ML
--- a/src/Pure/Isar/obtain.ML	Sat Sep 29 16:51:04 2012 +0200
+++ b/src/Pure/Isar/obtain.ML	Sat Sep 29 18:23:46 2012 +0200
@@ -232,7 +232,7 @@
       handle Type.TUNIFY =>
         err ("Failed to unify variable " ^
           string_of_term (Free (x, Envir.norm_type tyenv T)) ^ " against parameter " ^
-          string_of_term (Syntax_Trans.mark_boundT (y, Envir.norm_type tyenv U)) ^ " in") rule;
+          string_of_term (Syntax_Trans.mark_bound_abs (y, Envir.norm_type tyenv U)) ^ " in") rule;
     val (tyenv, _) = fold unify (map #1 vars ~~ take m params)
       (Vartab.empty, Int.max (maxidx, Thm.maxidx_of rule));
     val norm_type = Envir.norm_type tyenv;
diff -r 251342b60a82 -r de49d9b4d7bc src/Pure/Syntax/syntax_phases.ML
--- a/src/Pure/Syntax/syntax_phases.ML	Sat Sep 29 16:51:04 2012 +0200
+++ b/src/Pure/Syntax/syntax_phases.ML	Sat Sep 29 18:23:46 2012 +0200
@@ -550,8 +550,12 @@
           Ast.mk_appl (constrain (c $ Syntax.free x) T) (map ast_of ts)
       | ((c as Const ("_var", _)), Var (xi, T) :: ts) =>
           Ast.mk_appl (constrain (c $ Syntax.var xi) T) (map ast_of ts)
-      | ((c as Const ("_bound", _)), Free (x, T) :: ts) =>
-          Ast.mk_appl (constrain (c $ Syntax.free x) T) (map ast_of ts)
+      | ((c as Const ("_bound", B)), Free (x, T) :: ts) =>
+          let
+            val X =
+              if show_markup andalso not show_types orelse B <> dummyT then T
+              else dummyT;
+          in Ast.mk_appl (constrain (c $ Syntax.free x) X) (map ast_of ts) end
       | (Const ("_idtdummy", T), ts) =>
           Ast.mk_appl (constrain (Syntax.const "_idtdummy") T) (map ast_of ts)
       | (const as Const (c, T), ts) =>
diff -r 251342b60a82 -r de49d9b4d7bc src/Pure/Syntax/syntax_trans.ML
--- a/src/Pure/Syntax/syntax_trans.ML	Sat Sep 29 16:51:04 2012 +0200
+++ b/src/Pure/Syntax/syntax_trans.ML	Sat Sep 29 18:23:46 2012 +0200
@@ -30,8 +30,8 @@
   val applC_ast_tr': Ast.ast * Ast.ast list -> Ast.ast
   val eta_contract_default: bool Unsynchronized.ref
   val eta_contract_raw: Config.raw
-  val mark_bound: string -> term
-  val mark_boundT: string * typ -> term
+  val mark_bound_abs: string * typ -> term
+  val mark_bound_body: string * typ -> term
   val bound_vars: (string * typ) list -> term -> term
   val abs_tr': Proof.context -> term -> term
   val atomic_abs_tr': string * typ * term -> term * term
@@ -312,11 +312,11 @@
 
 (* abstraction *)
 
-fun mark_boundT (x, T) = Const ("_bound", T --> T) $ Free (x, T);
-fun mark_bound x = mark_boundT (x, dummyT);
+fun mark_bound_abs (x, T) = Const ("_bound", T --> T) $ Free (x, T);
+fun mark_bound_body (x, T) = Const ("_bound", dummyT) $ Free (x, T);
 
 fun bound_vars vars body =
-  subst_bounds (map mark_boundT (Term.rename_wrt_term body vars), body);
+  subst_bounds (map mark_bound_abs (Term.rename_wrt_term body vars), body);
 
 fun strip_abss vars_of body_of tm =
   let
@@ -326,7 +326,7 @@
     fun subst (x, T) b =
       if can Name.dest_internal x andalso not (Term.is_dependent b)
       then (Const ("_idtdummy", T), incr_boundvars ~1 b)
-      else (mark_boundT (x, T), Term.subst_bound (mark_bound x, 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;
   in (rev rev_vars', body') end;
 
@@ -337,7 +337,7 @@
 
 fun atomic_abs_tr' (x, T, t) =
   let val [xT] = Term.rename_wrt_term t [(x, T)]
-  in (mark_boundT xT, subst_bound (mark_bound (fst xT), t)) end;
+  in (mark_bound_abs xT, subst_bound (mark_bound_body xT, t)) end;
 
 fun abs_ast_tr' asts =
   (case Ast.unfold_ast_p "_abs" (Ast.Appl (Ast.Constant "_abs" :: asts)) of
@@ -437,12 +437,12 @@
   in (x', subst_bound (mark (x', T), b)) end;
 
 val variant_abs = var_abs Free;
-val variant_abs' = var_abs mark_boundT;
+val variant_abs' = var_abs mark_bound_abs;
 
 fun dependent_tr' (q, r) (A :: Abs (x, T, B) :: ts) =
       if Term.is_dependent B then
         let val (x', B') = variant_abs' (x, dummyT, B);
-        in Term.list_comb (Syntax.const q $ mark_boundT (x', T) $ A $ B', ts) end
+        in Term.list_comb (Syntax.const q $ mark_bound_abs (x', T) $ A $ B', ts) end
       else Term.list_comb (Syntax.const r $ A $ incr_boundvars ~1 B, ts)
   | dependent_tr' _ _ = raise Match;
 
diff -r 251342b60a82 -r de49d9b4d7bc src/Pure/raw_simplifier.ML
--- a/src/Pure/raw_simplifier.ML	Sat Sep 29 16:51:04 2012 +0200
+++ b/src/Pure/raw_simplifier.ML	Sat Sep 29 18:23:46 2012 +0200
@@ -302,7 +302,7 @@
   let
     val names = Term.declare_term_names t Name.context;
     val xs = rev (#1 (fold_map Name.variant (rev (map #2 bs)) names));
-    fun subst (((b, T), _), x') = (Free (b, T), Syntax_Trans.mark_boundT (x', T));
+    fun subst (((b, T), _), x') = (Free (b, T), Syntax_Trans.mark_bound_abs (x', T));
   in Term.subst_atomic (ListPair.map subst (bs, xs)) t end;
 
 fun print_term ss warn a t ctxt = prnt ss warn (a () ^ "\n" ^
diff -r 251342b60a82 -r de49d9b4d7bc src/Pure/type_infer_context.ML
--- a/src/Pure/type_infer_context.ML	Sat Sep 29 16:51:04 2012 +0200
+++ b/src/Pure/type_infer_context.ML	Sat Sep 29 18:23:46 2012 +0200
@@ -246,7 +246,7 @@
         val (Ts', Ts'') = chop (length Ts) Ts_bTs';
         fun prep t =
           let val xs = rev (Term.variant_frees t (rev (map fst bs ~~ Ts'')))
-          in Term.subst_bounds (map Syntax_Trans.mark_boundT xs, t) end;
+          in Term.subst_bounds (map Syntax_Trans.mark_bound_abs xs, t) end;
       in (map prep ts', Ts') end;
 
     fun err_loose i = error ("Loose bound variable: B." ^ string_of_int i);
diff -r 251342b60a82 -r de49d9b4d7bc src/Tools/induct.ML
--- a/src/Tools/induct.ML	Sat Sep 29 16:51:04 2012 +0200
+++ b/src/Tools/induct.ML	Sat Sep 29 18:23:46 2012 +0200
@@ -597,7 +597,7 @@
   in
     if not (null params) then
       (warning ("Cannot determine rule instantiation due to pending parameter(s): " ^
-        commas_quote (map (Syntax.string_of_term ctxt o Syntax_Trans.mark_boundT) params));
+        commas_quote (map (Syntax.string_of_term ctxt o Syntax_Trans.mark_bound_abs) params));
       Seq.single rule)
     else
       let
diff -r 251342b60a82 -r de49d9b4d7bc src/Tools/subtyping.ML
--- a/src/Tools/subtyping.ML	Sat Sep 29 16:51:04 2012 +0200
+++ b/src/Tools/subtyping.ML	Sat Sep 29 18:23:46 2012 +0200
@@ -231,7 +231,7 @@
     val (Ts', Ts'') = chop (length Ts) Ts_bTs';
     fun prep t =
       let val xs = rev (Term.variant_frees t (rev (map fst bs ~~ Ts'')))
-      in Term.subst_bounds (map Syntax_Trans.mark_boundT xs, t) end;
+      in Term.subst_bounds (map Syntax_Trans.mark_bound_abs xs, t) end;
   in (map prep ts', Ts') end;
 
 fun err_loose i = error ("Loose bound variable: B." ^ string_of_int i);