1.1 --- a/src/HOL/Tools/Nitpick/nitpick.ML	Tue Sep 03 11:58:34 2013 +0200
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick.ML	Tue Sep 03 13:09:15 2013 +0200
     1.3 @@ -460,7 +460,7 @@
     1.4        exists (exists (curry (op =) name o shortest_name o fst)
     1.5                o datatype_constrs hol_ctxt) deep_dataTs
     1.6      val likely_in_struct_induct_step =
     1.7 -      exists is_struct_induct_step (Proof_Context.cases_of ctxt)
     1.8 +      exists is_struct_induct_step (Proof_Context.dest_cases ctxt)
     1.9      val _ = if standard andalso likely_in_struct_induct_step then
    1.10                pprint_nt (fn () => Pretty.blk (0,
    1.11                    pstrs "Hint: To check that the induction hypothesis is \

     2.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Tue Sep 03 11:58:34 2013 +0200
     2.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Tue Sep 03 13:09:15 2013 +0200
     2.3 @@ -1600,7 +1600,7 @@
     2.4      val case_env = map2 (fn p => fn c => (Long_Name.base_name p, SOME c)) preds cases
     2.5      val lthy'' = lthy'
     2.6        |> fold Variable.auto_fixes cases_rules
     2.7 -      |> Proof_Context.add_cases true case_env
     2.8 +      |> Proof_Context.update_cases true case_env
     2.9      fun after_qed thms goal_ctxt =
    2.10        let
    2.11          val global_thms = Proof_Context.export goal_ctxt

     3.1 --- a/src/Pure/Isar/isar_syn.ML	Tue Sep 03 11:58:34 2013 +0200
     3.2 +++ b/src/Pure/Isar/isar_syn.ML	Tue Sep 03 13:09:15 2013 +0200
     3.3 @@ -611,8 +611,9 @@
     3.4  val _ =
     3.5    Outer_Syntax.command @{command_spec "case"} "invoke local context"
     3.6      ((@{keyword "("} |--
     3.7 -      Parse.!!! (Parse.xname -- Scan.repeat (Parse.maybe Parse.binding) --| @{keyword ")"}) ||
     3.8 -      Parse.xname >> rpair []) -- Parse_Spec.opt_attribs >> (fn ((c, xs), atts) =>
     3.9 +      Parse.!!! (Parse.position Parse.xname -- Scan.repeat (Parse.maybe Parse.binding)
    3.10 +        --| @{keyword ")"}) ||
    3.11 +      Parse.position Parse.xname >> rpair []) -- Parse_Spec.opt_attribs >> (fn ((c, xs), atts) =>
    3.12          Toplevel.print o Toplevel.proof (Proof.invoke_case_cmd (c, xs, atts))));
    3.13  
    3.14  

     4.1 --- a/src/Pure/Isar/proof.ML	Tue Sep 03 11:58:34 2013 +0200
     4.2 +++ b/src/Pure/Isar/proof.ML	Tue Sep 03 13:09:15 2013 +0200
     4.3 @@ -70,8 +70,10 @@
     4.4    val using_cmd: ((Facts.ref * Attrib.src list) list) list -> state -> state
     4.5    val unfolding: ((thm list * attribute list) list) list -> state -> state
     4.6    val unfolding_cmd: ((Facts.ref * Attrib.src list) list) list -> state -> state
     4.7 -  val invoke_case: string * binding option list * attribute list -> state -> state
     4.8 -  val invoke_case_cmd: string * binding option list * Attrib.src list -> state -> state
     4.9 +  val invoke_case: (string * Position.T) * binding option list * attribute list ->
    4.10 +    state -> state
    4.11 +  val invoke_case_cmd: (string * Position.T) * binding option list * Attrib.src list ->
    4.12 +    state -> state
    4.13    val begin_block: state -> state
    4.14    val next_block: state -> state
    4.15    val end_block: state -> state
    4.16 @@ -399,8 +401,8 @@
    4.17      Method.apply meth ctxt using goal |> Seq.map (fn (meth_cases, goal') =>
    4.18        state
    4.19        |> map_goal
    4.20 -          (Proof_Context.add_cases false (no_goal_cases goal @ goal_cases goal') #>
    4.21 -           Proof_Context.add_cases true meth_cases)
    4.22 +          (Proof_Context.update_cases false (no_goal_cases goal @ goal_cases goal') #>
    4.23 +           Proof_Context.update_cases true meth_cases)
    4.24            (K (statement, [], using, goal', before_qed, after_qed)) I)
    4.25    end;
    4.26  
    4.27 @@ -744,17 +746,17 @@
    4.28  fun qualified_binding a =
    4.29    Binding.qualify true (Long_Name.qualifier a) (Binding.name (Long_Name.base_name a));
    4.30  
    4.31 -fun gen_invoke_case prep_att (name, xs, raw_atts) state =
    4.32 +fun gen_invoke_case prep_att ((name, pos), xs, raw_atts) state =
    4.33    let
    4.34      val atts = map (prep_att (context_of state)) raw_atts;
    4.35      val (asms, state') = state |> map_context_result (fn ctxt =>
    4.36 -      ctxt |> Proof_Context.apply_case (Proof_Context.get_case ctxt name xs));
    4.37 +      ctxt |> Proof_Context.apply_case (Proof_Context.check_case ctxt (name, pos) xs));
    4.38      val assumptions = asms |> map (fn (a, ts) => ((qualified_binding a, atts), map (rpair []) ts));
    4.39    in
    4.40      state'
    4.41      |> assume assumptions
    4.42      |> bind_terms Auto_Bind.no_facts
    4.43 -    |> `the_facts |-> (fn thms => note_thmss [((Binding.name name, []), [(thms, [])])])
    4.44 +    |> `the_facts |-> (fn thms => note_thmss [((Binding.make (name, pos), []), [(thms, [])])])
    4.45    end;
    4.46  
    4.47  in

     5.1 --- a/src/Pure/Isar/proof_context.ML	Tue Sep 03 11:58:34 2013 +0200
     5.2 +++ b/src/Pure/Isar/proof_context.ML	Tue Sep 03 13:09:15 2013 +0200
     5.3 @@ -31,7 +31,6 @@
     5.4    val set_syntax_mode: Syntax.mode -> Proof.context -> Proof.context
     5.5    val restore_syntax_mode: Proof.context -> Proof.context -> Proof.context
     5.6    val facts_of: Proof.context -> Facts.T
     5.7 -  val cases_of: Proof.context -> (string * (Rule_Cases.T * bool)) list
     5.8    val map_naming: (Name_Space.naming -> Name_Space.naming) -> Proof.context -> Proof.context
     5.9    val naming_of: Proof.context -> Name_Space.naming
    5.10    val restore_naming: Proof.context -> Proof.context -> Proof.context
    5.11 @@ -132,9 +131,10 @@
    5.12    val add_assms_i: Assumption.export ->
    5.13      (Thm.binding * (term * term list) list) list ->
    5.14      Proof.context -> (string * thm list) list * Proof.context
    5.15 -  val add_cases: bool -> (string * Rule_Cases.T option) list -> Proof.context -> Proof.context
    5.16 +  val dest_cases: Proof.context -> (string * (Rule_Cases.T * bool)) list
    5.17 +  val update_cases: bool -> (string * Rule_Cases.T option) list -> Proof.context -> Proof.context
    5.18    val apply_case: Rule_Cases.T -> Proof.context -> (string * term list) list * Proof.context
    5.19 -  val get_case: Proof.context -> string -> binding option list -> Rule_Cases.T
    5.20 +  val check_case: Proof.context -> string * Position.T -> binding option list -> Rule_Cases.T
    5.21    val type_notation: bool -> Syntax.mode -> (typ * mixfix) list -> Proof.context -> Proof.context
    5.22    val notation: bool -> Syntax.mode -> (term * mixfix) list -> Proof.context -> Proof.context
    5.23    val generic_type_notation: bool -> Syntax.mode -> (typ * mixfix) list -> morphism ->
    5.24 @@ -192,6 +192,9 @@
    5.25  
    5.26  (** Isar proof context information **)
    5.27  
    5.28 +type cases = ((Rule_Cases.T * bool) * int) Name_Space.table;
    5.29 +val empty_cases: cases = Name_Space.empty_table Markup.caseN;
    5.30 +
    5.31  datatype data =
    5.32    Data of
    5.33     {mode: mode,                  (*inner syntax mode*)
    5.34 @@ -199,7 +202,7 @@
    5.35      tsig: Type.tsig * Type.tsig, (*local/global type signature -- local name space / defsort only*)
    5.36      consts: Consts.T * Consts.T, (*local/global consts -- local name space / abbrevs only*)
    5.37      facts: Facts.T,              (*local facts*)
    5.38 -    cases: (string * (Rule_Cases.T * bool)) list};    (*named case contexts*)
    5.39 +    cases: cases};               (*named case contexts: case, is_proper, running index*)
    5.40  
    5.41  fun make_data (mode, syntax, tsig, consts, facts, cases) =
    5.42    Data {mode = mode, syntax = syntax, tsig = tsig, consts = consts, facts = facts, cases = cases};
    5.43 @@ -210,7 +213,7 @@
    5.44    fun init thy =
    5.45      make_data (mode_default, Local_Syntax.init thy,
    5.46        (Sign.tsig_of thy, Sign.tsig_of thy),
    5.47 -      (Sign.consts_of thy, Sign.consts_of thy), Facts.empty, []);
    5.48 +      (Sign.consts_of thy, Sign.consts_of thy), Facts.empty, empty_cases);
    5.49  );
    5.50  
    5.51  fun rep_data ctxt = Data.get ctxt |> (fn Data rep => rep);
    5.52 @@ -1132,28 +1135,23 @@
    5.53  
    5.54  (** cases **)
    5.55  
    5.56 +fun dest_cases ctxt =
    5.57 +  Symtab.fold (fn (a, (c, i)) => cons (i, (a, c))) (#2 (cases_of ctxt)) []
    5.58 +  |> sort (int_ord o pairself #1) |> map #2;
    5.59 +
    5.60  local
    5.61  
    5.62 -fun rem_case name = remove (fn (x: string, (y, _)) => x = y) name;
    5.63 -
    5.64 -fun add_case _ ("", _) cases = cases
    5.65 -  | add_case _ (name, NONE) cases = rem_case name cases
    5.66 -  | add_case is_proper (name, SOME c) cases = (name, (c, is_proper)) :: rem_case name cases;
    5.67 -
    5.68 -fun prep_case name fxs c =
    5.69 -  let
    5.70 -    fun replace (opt_x :: xs) ((y, T) :: ys) = (the_default y opt_x, T) :: replace xs ys
    5.71 -      | replace [] ys = ys
    5.72 -      | replace (_ :: _) [] = error ("Too many parameters for case " ^ quote name);
    5.73 -    val Rule_Cases.Case {fixes, assumes, binds, cases} = c;
    5.74 -    val fixes' = replace fxs fixes;
    5.75 -    val binds' = map drop_schematic binds;
    5.76 -  in
    5.77 -    if null (fold (Term.add_tvarsT o snd) fixes []) andalso
    5.78 -      null (fold (fold Term.add_vars o snd) assumes []) then
    5.79 -        Rule_Cases.Case {fixes = fixes', assumes = assumes, binds = binds', cases = cases}
    5.80 -    else error ("Illegal schematic variable(s) in case " ^ quote name)
    5.81 -  end;
    5.82 +fun update_case _ _ ("", _) res = res
    5.83 +  | update_case _ _ (name, NONE) ((space, tab), index) =
    5.84 +      let
    5.85 +        val tab' = Symtab.delete_safe name tab;
    5.86 +      in ((space, tab'), index) end
    5.87 +  | update_case context is_proper (name, SOME c) (cases, index) =
    5.88 +      let
    5.89 +        val (_, cases') = cases |> Name_Space.define context false
    5.90 +          (Binding.make (name, Position.none), ((c, is_proper), index));
    5.91 +        val index' = index + 1;
    5.92 +      in (cases', index') end;
    5.93  
    5.94  fun fix (b, T) ctxt =
    5.95    let val ([x], ctxt') = add_fixes [(b, SOME T, NoSyn)] ctxt
    5.96 @@ -1161,7 +1159,13 @@
    5.97  
    5.98  in
    5.99  
   5.100 -fun add_cases is_proper = map_cases o fold (add_case is_proper);
   5.101 +fun update_cases is_proper args ctxt =
   5.102 +  let
   5.103 +    val context = Context.Proof ctxt |> Name_Space.map_naming (K Name_Space.default_naming);
   5.104 +    val cases = cases_of ctxt;
   5.105 +    val index = Symtab.fold (fn _ => Integer.add 1) (#2 cases) 0;
   5.106 +    val (cases', _) = fold (update_case context is_proper) args (cases, index);
   5.107 +  in map_cases (K cases') ctxt end;
   5.108  
   5.109  fun case_result c ctxt =
   5.110    let
   5.111 @@ -1171,16 +1175,29 @@
   5.112    in
   5.113      ctxt'
   5.114      |> bind_terms (map drop_schematic binds)
   5.115 -    |> add_cases true (map (apsnd SOME) cases)
   5.116 +    |> update_cases true (map (apsnd SOME) cases)
   5.117      |> pair (assumes, (binds, cases))
   5.118    end;
   5.119  
   5.120  val apply_case = apfst fst oo case_result;
   5.121  
   5.122 -fun get_case ctxt name xs =
   5.123 -  (case AList.lookup (op =) (cases_of ctxt) name of
   5.124 -    NONE => error ("Unknown case: " ^ quote name)
   5.125 -  | SOME (c, _) => prep_case name xs c);
   5.126 +fun check_case ctxt (name, pos) fxs =
   5.127 +  let
   5.128 +    val (_, ((Rule_Cases.Case {fixes, assumes, binds, cases}, _), _)) =
   5.129 +      Name_Space.check (Context.Proof ctxt) (cases_of ctxt) (name, pos);
   5.130 +
   5.131 +    fun replace (opt_x :: xs) ((y, T) :: ys) = (the_default y opt_x, T) :: replace xs ys
   5.132 +      | replace [] ys = ys
   5.133 +      | replace (_ :: _) [] =
   5.134 +          error ("Too many parameters for case " ^ quote name ^ Position.here pos);
   5.135 +    val fixes' = replace fxs fixes;
   5.136 +    val binds' = map drop_schematic binds;
   5.137 +  in
   5.138 +    if null (fold (Term.add_tvarsT o snd) fixes []) andalso
   5.139 +      null (fold (fold Term.add_vars o snd) assumes []) then
   5.140 +        Rule_Cases.Case {fixes = fixes', assumes = assumes, binds = binds', cases = cases}
   5.141 +    else error ("Illegal schematic variable(s) in case " ^ quote name ^ Position.here pos)
   5.142 +  end;
   5.143  
   5.144  end;
   5.145  
   5.146 @@ -1278,10 +1295,10 @@
   5.147  
   5.148  fun pretty_cases ctxt =
   5.149    let
   5.150 -    fun add_case (_, (_, false)) = I
   5.151 -      | add_case (name, (c as Rule_Cases.Case {fixes, ...}, true)) =
   5.152 -          cons (name, (fixes, case_result c ctxt));
   5.153 -    val cases = fold add_case (cases_of ctxt) [];
   5.154 +    fun mk_case (_, (_, false)) = NONE
   5.155 +      | mk_case (name, (c as Rule_Cases.Case {fixes, ...}, true)) =
   5.156 +          SOME (name, (fixes, case_result c ctxt));
   5.157 +    val cases = dest_cases ctxt |> map_filter mk_case;
   5.158    in
   5.159      if null cases then []
   5.160      else [Pretty.big_list "cases:" (map pretty_case cases)]

     6.1 --- a/src/Pure/PIDE/markup.ML	Tue Sep 03 11:58:34 2013 +0200
     6.2 +++ b/src/Pure/PIDE/markup.ML	Tue Sep 03 13:09:15 2013 +0200
     6.3 @@ -46,6 +46,7 @@
     6.4    val type_nameN: string
     6.5    val constantN: string
     6.6    val fixedN: string val fixed: string -> T
     6.7 +  val caseN: string val case_: string -> T
     6.8    val dynamic_factN: string val dynamic_fact: string -> T
     6.9    val tfreeN: string val tfree: T
    6.10    val tvarN: string val tvar: T
    6.11 @@ -288,6 +289,7 @@
    6.12  val constantN = "constant";
    6.13  
    6.14  val (fixedN, fixed) = markup_string "fixed" nameN;
    6.15 +val (caseN, case_) = markup_string "case" nameN;
    6.16  val (dynamic_factN, dynamic_fact) = markup_string "dynamic_fact" nameN;
    6.17  
    6.18  

     7.1 --- a/src/Pure/PIDE/markup.scala	Tue Sep 03 11:58:34 2013 +0200
     7.2 +++ b/src/Pure/PIDE/markup.scala	Tue Sep 03 13:09:15 2013 +0200
     7.3 @@ -105,8 +105,8 @@
     7.4    val CLASS = "class"
     7.5    val TYPE_NAME = "type_name"
     7.6    val FIXED = "fixed"
     7.7 +  val CASE = "case"
     7.8    val CONSTANT = "constant"
     7.9 -
    7.10    val DYNAMIC_FACT = "dynamic_fact"
    7.11  
    7.12