more precise position information via Variable.add_fixes_binding;

--- a/src/HOL/Tools/inductive.ML	Wed Apr 27 19:55:42 2011 +0200
+++ b/src/HOL/Tools/inductive.ML	Wed Apr 27 20:19:05 2011 +0200
@@ -552,10 +552,10 @@
 val ind_cases_setup =
   Method.setup @{binding ind_cases}
     (Scan.lift (Scan.repeat1 Args.name_source --
-      Scan.optional (Args.$$$ "for" |-- Scan.repeat1 Args.name) []) >>
+      Scan.optional (Args.$$$ "for" |-- Scan.repeat1 Args.binding) []) >>
       (fn (raw_props, fixes) => fn ctxt =>
         let
-          val (_, ctxt') = Variable.add_fixes fixes ctxt;
+          val (_, ctxt') = Variable.add_fixes_binding fixes ctxt;
           val props = Syntax.read_props ctxt' raw_props;
           val ctxt'' = fold Variable.declare_term props ctxt';
           val rules = Proof_Context.export ctxt'' ctxt (map (mk_cases ctxt'') props)

--- a/src/Pure/Isar/proof_context.ML	Wed Apr 27 19:55:42 2011 +0200
+++ b/src/Pure/Isar/proof_context.ML	Wed Apr 27 20:19:05 2011 +0200
@@ -1027,15 +1027,16 @@
 
 fun add_fixes raw_vars ctxt =
   let
-    val (vars, _) = cert_vars raw_vars ctxt;
-    val (xs', ctxt') = Variable.add_fixes (map (Variable.name o #1) vars) ctxt;
-    val ctxt'' =
-      ctxt'
-      |> fold_map declare_var (map2 (fn x' => fn (_, T, mx) => (x', T, mx)) xs' vars)
-      |-> (map_syntax o Local_Syntax.add_syntax (theory_of ctxt) o map (pair Local_Syntax.Fixed));
-    val _ = (vars ~~ xs') |> List.app (fn ((b, _, _), x') =>
-      Context_Position.report ctxt (Binding.pos_of b) (Markup.fixed_decl x'));
-  in (xs', ctxt'') end;
+    val thy = theory_of ctxt;
+    val vars = #1 (cert_vars raw_vars ctxt);
+  in
+    ctxt
+    |> Variable.add_fixes_binding (map #1 vars)
+    |-> (fn xs =>
+      fold_map declare_var (map2 (fn x => fn (_, T, mx) => (x, T, mx)) xs vars)
+      #-> (map_syntax o Local_Syntax.add_syntax thy o map (pair Local_Syntax.Fixed))
+      #> pair xs)
+  end;
 
 
 (* fixes vs. frees *)