# HG changeset patch
# User wenzelm
# Date 1303938163 -7200
# Node ID 65ec88b369fdf7b7f45e56b84c2a1f8cda5879f9
# Parent  1af81b70cf098bdbd8b74fa7f2db0726b0c92083
more precise positions via binding;

diff -r 1af81b70cf09 -r 65ec88b369fd src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Wed Apr 27 21:50:04 2011 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Wed Apr 27 23:02:43 2011 +0200
@@ -632,7 +632,7 @@
 
 val case_spec =
   (Parse.$$$ "(" |--
-    Parse.!!! (Parse.xname -- Scan.repeat1 (Parse.maybe Parse.name) --| Parse.$$$ ")") ||
+    Parse.!!! (Parse.xname -- Scan.repeat1 (Parse.maybe Parse.binding) --| Parse.$$$ ")") ||
     Parse.xname >> rpair []) -- Parse_Spec.opt_attribs >> Parse.triple1;
 
 val _ =
diff -r 1af81b70cf09 -r 65ec88b369fd src/Pure/Isar/local_defs.ML
--- a/src/Pure/Isar/local_defs.ML	Wed Apr 27 21:50:04 2011 +0200
+++ b/src/Pure/Isar/local_defs.ML	Wed Apr 27 23:02:43 2011 +0200
@@ -8,7 +8,7 @@
 sig
   val cert_def: Proof.context -> term -> (string * typ) * term
   val abs_def: term -> (string * typ) * term
-  val mk_def: Proof.context -> (string * term) list -> term list
+  val mk_def: Proof.context -> (binding * term) list -> term list
   val expand: cterm list -> thm -> thm
   val def_export: Assumption.export
   val add_defs: ((binding * mixfix) * (Thm.binding * term)) list -> Proof.context ->
@@ -59,7 +59,7 @@
   let
     val (xs, rhss) = split_list args;
     val (bind, _) = Proof_Context.bind_fixes xs ctxt;
-    val lhss = map (fn (x, rhs) => bind (Free (x, Term.fastype_of rhs))) args;
+    val lhss = map (fn (x, rhs) => bind (Free (Binding.name_of x, Term.fastype_of rhs))) args;
   in map Logic.mk_equals (lhss ~~ rhss) end;
 
 
@@ -90,15 +90,14 @@
 
 fun add_defs defs ctxt =
   let
-    val ((bvars, mxs), specs) = defs |> split_list |>> split_list;
+    val ((xs, mxs), specs) = defs |> split_list |>> split_list;
     val ((bfacts, atts), rhss) = specs |> split_list |>> split_list;
-    val xs = map Variable.check_name bvars;
-    val names = map2 Thm.def_binding_optional bvars bfacts;
+    val names = map2 Thm.def_binding_optional xs bfacts;
     val eqs = mk_def ctxt (xs ~~ rhss);
     val lhss = map (fst o Logic.dest_equals) eqs;
   in
     ctxt
-    |> Proof_Context.add_fixes (map2 (fn x => fn mx => (x, NONE, mx)) bvars mxs) |> #2
+    |> Proof_Context.add_fixes (map2 (fn x => fn mx => (x, NONE, mx)) xs mxs) |> #2
     |> fold Variable.declare_term eqs
     |> Proof_Context.add_assms_i def_export
       (map2 (fn a => fn eq => (a, [(eq, [])])) (names ~~ atts) eqs)
diff -r 1af81b70cf09 -r 65ec88b369fd src/Pure/Isar/obtain.ML
--- a/src/Pure/Isar/obtain.ML	Wed Apr 27 21:50:04 2011 +0200
+++ b/src/Pure/Isar/obtain.ML	Wed Apr 27 23:02:43 2011 +0200
@@ -99,7 +99,7 @@
 
 fun bind_judgment ctxt name =
   let
-    val (bind, ctxt') = Proof_Context.bind_fixes [name] ctxt;
+    val (bind, ctxt') = Proof_Context.bind_fixes [Binding.name name] ctxt;
     val (t as _ $ Free v) = bind (Object_Logic.fixed_judgment (Proof_Context.theory_of ctxt) name);
   in ((v, t), ctxt') end;
 
@@ -278,7 +278,7 @@
       let
         val ((parms, rule), ctxt') =
           unify_params vars thesis_var raw_rule (Proof.context_of state');
-        val (bind, _) = Proof_Context.bind_fixes (map (#1 o #1) parms) ctxt';
+        val (bind, _) = Proof_Context.bind_fixes (map (Binding.name o #1 o #1) parms) ctxt';
         val ts = map (bind o Free o #1) parms;
         val ps = map dest_Free ts;
         val asms =
diff -r 1af81b70cf09 -r 65ec88b369fd src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Wed Apr 27 21:50:04 2011 +0200
+++ b/src/Pure/Isar/proof.ML	Wed Apr 27 23:02:43 2011 +0200
@@ -71,8 +71,8 @@
   val using_cmd: ((Facts.ref * Attrib.src list) list) list -> state -> state
   val unfolding: ((thm list * attribute list) list) list -> state -> state
   val unfolding_cmd: ((Facts.ref * Attrib.src list) list) list -> state -> state
-  val invoke_case: string * string option list * attribute list -> state -> state
-  val invoke_case_cmd: string * string option list * Attrib.src list -> state -> state
+  val invoke_case: string * binding option list * attribute list -> state -> state
+  val invoke_case_cmd: string * binding option list * Attrib.src list -> state -> state
   val begin_block: state -> state
   val next_block: state -> state
   val end_block: state -> state
diff -r 1af81b70cf09 -r 65ec88b369fd src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Wed Apr 27 21:50:04 2011 +0200
+++ b/src/Pure/Isar/proof_context.ML	Wed Apr 27 23:02:43 2011 +0200
@@ -125,7 +125,7 @@
   val add_fixes: (binding * typ option * mixfix) list -> Proof.context ->
     string list * Proof.context
   val auto_fixes: Proof.context * (term list list * 'a) -> Proof.context * (term list list * 'a)
-  val bind_fixes: string list -> Proof.context -> (term -> term) * Proof.context
+  val bind_fixes: binding list -> Proof.context -> (term -> term) * Proof.context
   val add_assms: Assumption.export ->
     (Thm.binding * (string * string list) list) list ->
     Proof.context -> (string * thm list) list * Proof.context
@@ -134,7 +134,7 @@
     Proof.context -> (string * thm list) list * Proof.context
   val add_cases: bool -> (string * Rule_Cases.T option) list -> Proof.context -> Proof.context
   val apply_case: Rule_Cases.T -> Proof.context -> (string * term list) list * Proof.context
-  val get_case: Proof.context -> string -> string option list -> Rule_Cases.T
+  val get_case: Proof.context -> string -> binding option list -> Rule_Cases.T
   val type_notation: bool -> Syntax.mode -> (typ * mixfix) list -> Proof.context -> Proof.context
   val notation: bool -> Syntax.mode -> (term * mixfix) list -> Proof.context -> Proof.context
   val target_type_notation: bool -> Syntax.mode -> (typ * mixfix) list -> morphism ->
@@ -1044,9 +1044,10 @@
 fun auto_fixes (ctxt, (propss, x)) =
   ((fold o fold) Variable.auto_fixes propss ctxt, (propss, x));
 
-fun bind_fixes xs ctxt =
+fun bind_fixes bs ctxt =
   let
-    val (_, ctxt') = ctxt |> add_fixes (map (fn x => (Binding.name x, NONE, NoSyn)) xs);
+    val (_, ctxt') = ctxt |> add_fixes (map (fn b => (b, NONE, NoSyn)) bs);
+    val xs = map Binding.name_of bs;
     fun bind (t as Free (x, T)) =
           if member (op =) xs x then
             (case Variable.lookup_fixed ctxt' x of SOME x' => Free (x', T) | NONE => t)
@@ -1111,7 +1112,7 @@
 fun fix (x, T) ctxt =
   let
     val (bind, ctxt') = bind_fixes [x] ctxt;
-    val t = bind (Free (x, T));
+    val t = bind (Free (Binding.name_of x, T));
   in (t, ctxt' |> Variable.declare_constraints t) end;
 
 in
@@ -1221,7 +1222,7 @@
   in
     Pretty.block (Pretty.fbreaks
       (Pretty.str (name ^ ":") ::
-        prt_sect "fix" [] (Pretty.str o fst) fixes @
+        prt_sect "fix" [] (Pretty.str o Binding.name_of o fst) fixes @
         prt_sect "let" [Pretty.str "and"] prt_let
           (map_filter (fn (xi, SOME t) => SOME (xi, t) | _ => NONE) lets) @
         (if forall (null o #2) asms then []
diff -r 1af81b70cf09 -r 65ec88b369fd src/Pure/Isar/rule_cases.ML
--- a/src/Pure/Isar/rule_cases.ML	Wed Apr 27 21:50:04 2011 +0200
+++ b/src/Pure/Isar/rule_cases.ML	Wed Apr 27 23:02:43 2011 +0200
@@ -20,7 +20,7 @@
 sig
   include BASIC_RULE_CASES
   datatype T = Case of
-   {fixes: (string * typ) list,
+   {fixes: (binding * typ) list,
     assumes: (string * term list) list,
     binds: (indexname * term option) list,
     cases: (string * T) list}
@@ -56,7 +56,7 @@
 (** cases **)
 
 datatype T = Case of
- {fixes: (string * typ) list,
+ {fixes: (binding * typ) list,
   assumes: (string * term list) list,
   binds: (indexname * term option) list,
   cases: (string * T) list};
@@ -93,6 +93,8 @@
         chop (length (Logic.strip_assums_hyp outline)) (Logic.strip_assums_hyp prop)
       in ([(qual case_hypsN, hyps)], [(qual case_premsN, prems)]) end;
 
+fun bindings args = map (apfst Binding.name) args;
+
 fun extract_case thy (case_outline, raw_prop) name concls =
   let
     val props = Logic.dest_conjunctions (Drule.norm_hhf thy raw_prop);
@@ -122,11 +124,12 @@
     val cases = map extract props;
 
     fun common_case ((fixes1, assumes1), ((fixes2, assumes2), binds)) =
-      Case {fixes = fixes1 @ fixes2, assumes = assumes1 @ assumes2, binds = binds, cases = []};
+      Case {fixes = bindings (fixes1 @ fixes2),
+        assumes = assumes1 @ assumes2, binds = binds, cases = []};
     fun inner_case (_, ((fixes2, assumes2), binds)) =
-      Case {fixes = fixes2, assumes = assumes2, binds = binds, cases = []};
+      Case {fixes = bindings fixes2, assumes = assumes2, binds = binds, cases = []};
     fun nested_case ((fixes1, assumes1), _) =
-      Case {fixes = fixes1, assumes = assumes1, binds = [],
+      Case {fixes = bindings fixes1, assumes = assumes1, binds = [],
         cases = map string_of_int (1 upto len) ~~ map inner_case cases};
   in
     if len = 0 then NONE