merged

--- a/NEWS	Tue Mar 24 18:10:56 2015 +0100
+++ b/NEWS	Tue Mar 24 23:39:42 2015 +0100
@@ -66,6 +66,10 @@
 these variables become schematic in the instantiated theorem. This
 behaviour is analogous to 'for' in attributes "where" and "of".
 
+* Explicit instantiation via attributes "where", "of", and proof methods
+"rule_tac" with derivatives like "subgoal_tac" etc. admit dummy patterns
+("_") that stand for anonymous local variables.
+
 * Command "class_deps" takes optional sort arguments constraining
 the search space.
 

--- a/src/HOL/HOLCF/Compact_Basis.thy	Tue Mar 24 18:10:56 2015 +0100
+++ b/src/HOL/HOLCF/Compact_Basis.thy	Tue Mar 24 23:39:42 2015 +0100
@@ -16,7 +16,7 @@
 
 typedef 'a pd_basis = "pd_basis :: 'a compact_basis set set"
   unfolding pd_basis_def
-  apply (rule_tac x="{a}" for a in exI)
+  apply (rule_tac x="{_}" in exI)
   apply simp
   done
 

--- a/src/HOL/MicroJava/J/JTypeSafe.thy	Tue Mar 24 18:10:56 2015 +0100
+++ b/src/HOL/MicroJava/J/JTypeSafe.thy	Tue Mar 24 23:39:42 2015 +0100
@@ -244,7 +244,7 @@
        THEN_ALL_NEW (full_simp_tac @{context}), REPEAT o (etac conjE), hyp_subst_tac @{context}] 3*})
 
 -- "for if"
-apply( tactic {* (Induct_Tacs.case_tac @{context} "the_Bool v" THEN_ALL_NEW
+apply( tactic {* (Induct_Tacs.case_tac @{context} "the_Bool v" [] THEN_ALL_NEW
   (asm_full_simp_tac @{context})) 7*})
 
 apply (tactic "forward_hyp_tac @{context}")

--- a/src/HOL/Nominal/nominal_atoms.ML	Tue Mar 24 18:10:56 2015 +0100
+++ b/src/HOL/Nominal/nominal_atoms.ML	Tue Mar 24 23:39:42 2015 +0100
@@ -131,7 +131,7 @@
                   (HOLogic.mk_exists ("x",@{typ nat},HOLogic.mk_eq (y,Const (ak_sign,inj_type) $ Bound 0)))
 
               val proof2 = fn {prems, context = ctxt} =>
-                Induct_Tacs.case_tac ctxt "y" 1 THEN
+                Induct_Tacs.case_tac ctxt "y" [] 1 THEN
                 asm_simp_tac (put_simpset HOL_basic_ss ctxt addsimps simp1) 1 THEN
                 rtac @{thm exI} 1 THEN
                 rtac @{thm refl} 1

--- a/src/HOL/TLA/Memory/MemoryImplementation.thy	Tue Mar 24 18:10:56 2015 +0100
+++ b/src/HOL/TLA/Memory/MemoryImplementation.thy	Tue Mar 24 23:39:42 2015 +0100
@@ -798,7 +798,7 @@
 fun split_idle_tac ctxt =
   SELECT_GOAL
    (TRY (rtac @{thm actionI} 1) THEN
-    Induct_Tacs.case_tac ctxt "(s,t) |= unchanged (e p, c p, r p, m p, rmhist!p)" 1 THEN
+    Induct_Tacs.case_tac ctxt "(s,t) |= unchanged (e p, c p, r p, m p, rmhist!p)" [] 1 THEN
     rewrite_goals_tac ctxt @{thms action_rews} THEN
     forward_tac ctxt [temp_use ctxt @{thm Step1_4_7}] 1 THEN
     asm_full_simp_tac ctxt 1);

--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Tue Mar 24 18:10:56 2015 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Tue Mar 24 23:39:42 2015 +0100
@@ -609,10 +609,13 @@
 fun is_free_in frees (Free (v, _)) = member (op =) frees v
   | is_free_in _ _ = false;
 
+fun is_catch_all_prem (Free (v, _)) = v = Name.uu_
+  | is_catch_all_prem _ = false;
+
 fun add_extra_frees ctxt frees names =
   fold_aterms (fn x as Free (v, _) =>
     (not (member (op =) frees x) andalso not (member (op =) names v) andalso
-     not (Variable.is_fixed ctxt v) andalso v <> Name.uu_)
+     not (Variable.is_fixed ctxt v) andalso not (is_catch_all_prem x))
     ? cons x | _ => I);
 
 fun check_extra_frees ctxt frees names t =
@@ -679,9 +682,6 @@
     val ctr_no = if not_disc then 1 - ctr_no' else ctr_no';
     val {ctr, disc, ...} = nth basic_ctr_specs ctr_no;
 
-    fun is_catch_all_prem (Free (s, _)) = s = Name.uu_
-      | is_catch_all_prem _ = false;
-
     val catch_all =
       (case prems0 of
         [prem] => is_catch_all_prem prem

--- a/src/Pure/Isar/proof_context.ML	Tue Mar 24 18:10:56 2015 +0100
+++ b/src/Pure/Isar/proof_context.ML	Tue Mar 24 23:39:42 2015 +0100
@@ -412,7 +412,7 @@
 
 fun read_class ctxt text =
   let
-    val source = Syntax.read_token text;
+    val source = Syntax.read_input text;
     val (c, reports) = check_class ctxt (Input.source_content source, Input.pos_of source);
     val _ = Position.reports reports;
   in c end;
@@ -480,7 +480,7 @@
 
 fun read_type_name ctxt flags text =
   let
-    val source = Syntax.read_token text;
+    val source = Syntax.read_input text;
     val (T, reports) =
       check_type_name ctxt flags (Input.source_content source, Input.pos_of source);
     val _ = Position.reports reports;
@@ -530,7 +530,7 @@
 
 fun read_const ctxt flags text =
   let
-    val source = Syntax.read_token text;
+    val source = Syntax.read_input text;
     val (t, reports) = check_const ctxt flags (Input.source_content source, [Input.pos_of source]);
     val _ = Position.reports reports;
   in t end;
@@ -945,7 +945,7 @@
 fun retrieve pick context (Facts.Fact s) =
       let
         val ctxt = Context.the_proof context;
-        val pos = Syntax.read_token_pos s;
+        val pos = Syntax.read_input_pos s;
         val prop =
           Syntax.read_prop (ctxt |> set_mode mode_default |> allow_dummies) s
           |> singleton (Variable.polymorphic ctxt);

--- a/src/Pure/Isar/token.ML	Tue Mar 24 18:10:56 2015 +0100
+++ b/src/Pure/Isar/token.ML	Tue Mar 24 23:39:42 2015 +0100
@@ -55,9 +55,9 @@
   val is_space: T -> bool
   val is_blank: T -> bool
   val is_newline: T -> bool
-  val inner_syntax_of: T -> string
+  val content_of: T -> string
   val source_position_of: T -> Input.source
-  val content_of: T -> string
+  val inner_syntax_of: T -> string
   val keyword_markup: bool * Markup.T -> string -> Markup.T
   val completion_report: T -> Position.report_text list
   val reports: Keyword.keywords -> T -> Position.report_text list
@@ -279,18 +279,14 @@
 
 (* token content *)
 
-fun inner_syntax_of (Token ((source, (pos, _)), (kind, x), _)) =
-  if YXML.detect x then x
-  else
-    let
-      val delimited = delimited_kind kind;
-      val tree = XML.Elem (Markup.token delimited (Position.properties_of pos), [XML.Text source]);
-    in YXML.string_of tree end;
+fun content_of (Token (_, (_, x), _)) = x;
 
 fun source_position_of (Token ((source, range), (kind, _), _)) =
   Input.source (delimited_kind kind) source range;
 
-fun content_of (Token (_, (_, x), _)) = x;
+fun inner_syntax_of tok =
+  let val x = content_of tok
+  in if YXML.detect x then x else Syntax.implode_input (source_position_of tok) end;
 
 
 (* markup reports *)

--- a/src/Pure/PIDE/markup.ML	Tue Mar 24 18:10:56 2015 +0100
+++ b/src/Pure/PIDE/markup.ML	Tue Mar 24 23:39:42 2015 +0100
@@ -114,13 +114,13 @@
   val document_antiquotation_optionN: string
   val paragraphN: string val paragraph: T
   val text_foldN: string val text_fold: T
+  val inputN: string val input: bool -> Properties.T -> T
   val commandN: string val command: T
   val stringN: string val string: T
   val alt_stringN: string val alt_string: T
   val verbatimN: string val verbatim: T
   val cartoucheN: string val cartouche: T
   val commentN: string val comment: T
-  val tokenN: string val token: bool -> Properties.T -> T
   val keyword1N: string val keyword1: T
   val keyword2N: string val keyword2: T
   val keyword3N: string val keyword3: T
@@ -456,6 +456,12 @@
 val (text_foldN, text_fold) = markup_elem "text_fold";
 
 
+(* formal input *)
+
+val inputN = "input";
+fun input delimited props = (inputN, (delimitedN, print_bool delimited) :: props);
+
+
 (* outer syntax *)
 
 val (commandN, command) = markup_elem "command";
@@ -471,9 +477,6 @@
 val (cartoucheN, cartouche) = markup_elem "cartouche";
 val (commentN, comment) = markup_elem "comment";
 
-val tokenN = "token";
-fun token delimited props = (tokenN, (delimitedN, print_bool delimited) :: props);
-
 
 (* timing *)
 

--- a/src/Pure/Syntax/syntax.ML	Tue Mar 24 18:10:56 2015 +0100
+++ b/src/Pure/Syntax/syntax.ML	Tue Mar 24 23:39:42 2015 +0100
@@ -14,9 +14,11 @@
   val ambiguity_warning: bool Config.T
   val ambiguity_limit_raw: Config.raw
   val ambiguity_limit: int Config.T
-  val read_token_pos: string -> Position.T
-  val read_token: string -> Input.source
-  val parse_token: Proof.context -> (XML.tree list -> 'a) ->
+  val encode_input: Input.source -> XML.tree
+  val implode_input: Input.source -> string
+  val read_input_pos: string -> Position.T
+  val read_input: string -> Input.source
+  val parse_input: Proof.context -> (XML.tree list -> 'a) ->
     (bool -> Markup.T) -> (Symbol_Pos.T list * Position.T -> 'a) -> string -> 'a
   val parse_sort: Proof.context -> string -> sort
   val parse_typ: Proof.context -> string -> typ
@@ -159,33 +161,42 @@
 val ambiguity_limit = Config.int ambiguity_limit_raw;
 
 
-(* outer syntax token -- with optional YXML content *)
+(* formal input *)
+
+fun encode_input source =
+  let
+    val delimited = Input.is_delimited source;
+    val pos = Input.pos_of source;
+    val text = Input.text_of source;
+  in XML.Elem (Markup.input delimited (Position.properties_of pos), [XML.Text text]) end;
+
+val implode_input = encode_input #> YXML.string_of;
 
 local
 
-fun token_range (XML.Elem ((name, props), _)) =
-      if name = Markup.tokenN
+fun input_range (XML.Elem ((name, props), _)) =
+      if name = Markup.inputN
       then (Markup.is_delimited props, Position.range_of_properties props)
       else (false, Position.no_range)
-  | token_range (XML.Text _) = (false, Position.no_range);
+  | input_range (XML.Text _) = (false, Position.no_range);
 
-fun token_source tree : Input.source =
+fun input_source tree =
   let
     val text = XML.content_of [tree];
-    val (delimited, range) = token_range tree;
+    val (delimited, range) = input_range tree;
   in Input.source delimited text range end;
 
 in
 
-fun read_token_pos str = #1 (#2 (token_range (YXML.parse str handle Fail msg => error msg)));
+fun read_input_pos str = #1 (#2 (input_range (YXML.parse str handle Fail msg => error msg)));
 
-fun read_token str = token_source (YXML.parse str handle Fail msg => error msg);
+fun read_input str = input_source (YXML.parse str handle Fail msg => error msg);
 
-fun parse_token ctxt decode markup parse str =
+fun parse_input ctxt decode markup parse str =
   let
     fun parse_tree tree =
       let
-        val source = token_source tree;
+        val source = input_source tree;
         val syms = Input.source_explode source;
         val pos = Input.pos_of source;
         val _ = Context_Position.report ctxt pos (markup (Input.is_delimited source));
@@ -193,7 +204,7 @@
   in
     (case YXML.parse_body str handle Fail msg => error msg of
       body as [tree as XML.Elem ((name, _), _)] =>
-        if name = Markup.tokenN then parse_tree tree else decode body
+        if name = Markup.inputN then parse_tree tree else decode body
     | [tree as XML.Text _] => parse_tree tree
     | body => decode body)
   end;

--- a/src/Pure/Syntax/syntax_phases.ML	Tue Mar 24 18:10:56 2015 +0100
+++ b/src/Pure/Syntax/syntax_phases.ML	Tue Mar 24 23:39:42 2015 +0100
@@ -365,7 +365,7 @@
     Markup.markup_report (Context_Position.reported_text ctxt pos Markup.bad ""));
 
 fun parse_sort ctxt =
-  Syntax.parse_token ctxt Term_XML.Decode.sort Markup.language_sort
+  Syntax.parse_input ctxt Term_XML.Decode.sort Markup.language_sort
     (fn (syms, pos) =>
       parse_tree ctxt "sort" (syms, pos)
       |> uncurry (report_result ctxt pos)
@@ -374,7 +374,7 @@
       handle ERROR msg => parse_failed ctxt pos msg "sort");
 
 fun parse_typ ctxt =
-  Syntax.parse_token ctxt Term_XML.Decode.typ Markup.language_type
+  Syntax.parse_input ctxt Term_XML.Decode.typ Markup.language_type
     (fn (syms, pos) =>
       parse_tree ctxt "type" (syms, pos)
       |> uncurry (report_result ctxt pos)
@@ -389,7 +389,7 @@
       else (Markup.language_term, "term", Config.get ctxt Syntax.root, I);
     val decode = constrain o Term_XML.Decode.term;
   in
-    Syntax.parse_token ctxt decode markup
+    Syntax.parse_input ctxt decode markup
       (fn (syms, pos) =>
         let
           val (ambig_msgs, results) = parse_tree ctxt root (syms, pos) ||> map (decode_term ctxt);
@@ -463,7 +463,7 @@
           else decode_appl ps asts
       | decode ps (Ast.Appl asts) = decode_appl ps asts;
 
-    val source = Syntax.read_token str;
+    val source = Syntax.read_input str;
     val pos = Input.pos_of source;
     val syms = Input.source_explode source;
     val ast =

--- a/src/Pure/Thy/thy_syntax.scala	Tue Mar 24 18:10:56 2015 +0100
+++ b/src/Pure/Thy/thy_syntax.scala	Tue Mar 24 23:39:42 2015 +0100
@@ -147,8 +147,8 @@
     : (List[Command], List[(Command.Blobs_Info, Command_Span.Span)]) =
   {
     (cmds, blobs_spans) match {
-      case (cmd :: cmds, (blobs, span) :: rest) if cmd.blobs == blobs && cmd.span == span =>
-        chop_common(cmds, rest)
+      case (cmd :: cmds, (blobs_info, span) :: rest)
+      if cmd.blobs_info == blobs_info && cmd.span == span => chop_common(cmds, rest)
       case _ => (cmds, blobs_spans)
     }
   }

--- a/src/Pure/Tools/rule_insts.ML	Tue Mar 24 18:10:56 2015 +0100
+++ b/src/Pure/Tools/rule_insts.ML	Tue Mar 24 23:39:42 2015 +0100
@@ -13,6 +13,7 @@
     (binding * string option * mixfix) list -> thm -> thm
   val read_instantiate: Proof.context ->
     ((indexname * Position.T) * string) list -> string list -> thm -> thm
+  val schematic: bool Config.T
   val res_inst_tac: Proof.context ->
     ((indexname * Position.T) * string) list -> (binding * string option * mixfix) list -> thm ->
     int -> tactic
@@ -68,18 +69,18 @@
     else error_var "Bad sort for instantiation of type variable: " (xi, pos)
   end;
 
-fun read_terms ctxt ss Ts =
+fun read_terms ss Ts ctxt =
   let
     fun parse T = if T = propT then Syntax.parse_prop ctxt else Syntax.parse_term ctxt;
-    val ts = map2 parse Ts ss;
+    val (ts, ctxt') = fold_map Variable.fix_dummy_patterns (map2 parse Ts ss) ctxt;
     val ts' =
       map2 (Type.constraint o Type_Infer.paramify_vars) Ts ts
-      |> Syntax.check_terms ctxt
-      |> Variable.polymorphic ctxt;
+      |> Syntax.check_terms ctxt'
+      |> Variable.polymorphic ctxt';
     val Ts' = map Term.fastype_of ts';
     val tyenv = fold Type.raw_match (Ts ~~ Ts') Vartab.empty;
     val tyenv' = Vartab.fold (fn (xi, (S, T)) => cons ((xi, S), T)) tyenv [];
-  in (ts', tyenv') end;
+  in ((ts', tyenv'), ctxt') end;
 
 fun make_instT f v =
   let
@@ -95,7 +96,7 @@
 
 in
 
-fun read_insts ctxt mixed_insts thm =
+fun read_insts thm mixed_insts ctxt =
   let
     val (type_insts, term_insts) =
       List.partition (fn (((x, _), _), _) => String.isPrefix "'" x) mixed_insts;
@@ -110,7 +111,7 @@
     (*term instantiations*)
     val (xs, ss) = split_list term_insts;
     val Ts = map (the_type vars1) xs;
-    val (ts, inferred) = read_terms ctxt ss Ts;
+    val ((ts, inferred), ctxt') = read_terms ss Ts ctxt;
 
     (*implicit type instantiations*)
     val instT2 = Term_Subst.instantiateT inferred;
@@ -121,7 +122,7 @@
 
     val inst_tvars = map_filter (make_instT (instT2 o instT1)) tvars;
     val inst_vars = map_filter (make_inst inst2) vars2;
-  in (inst_tvars, inst_vars) end;
+  in ((inst_tvars, inst_vars), ctxt') end;
 
 end;
 
@@ -134,13 +135,13 @@
     val ctxt' = ctxt
       |> Variable.declare_thm thm
       |> Proof_Context.read_vars fixes |-> Proof_Context.add_fixes |> #2;
-    val (inst_tvars, inst_vars) = read_insts ctxt' mixed_insts thm;
+    val ((inst_tvars, inst_vars), ctxt'') = read_insts thm mixed_insts ctxt';
   in
     thm
     |> Drule.instantiate_normalize
-      (map (apply2 (Thm.ctyp_of ctxt) o apfst TVar) inst_tvars,
-       map (apply2 (Thm.cterm_of ctxt) o apfst Var) inst_vars)
-    |> singleton (Variable.export ctxt' ctxt)
+      (map (apply2 (Thm.ctyp_of ctxt'') o apfst TVar) inst_tvars,
+       map (apply2 (Thm.cterm_of ctxt'') o apfst Var) inst_vars)
+    |> singleton (Variable.export ctxt'' ctxt)
     |> Rule_Cases.save thm
   end;
 
@@ -198,6 +199,8 @@
 
 (** tactics **)
 
+val schematic = Attrib.setup_config_bool @{binding rule_insts_schematic} (K true);
+
 (* resolution after lifting and instantiation; may refer to parameters of the subgoal *)
 
 fun bires_inst_tac bires_flag ctxt mixed_insts fixes thm i st = CSUBGOAL (fn (cgoal, _) =>
@@ -216,7 +219,7 @@
       |> Variable.improper_fixes
       |> Proof_Context.add_fixes (map (fn (x, T) => (Binding.name x, SOME T, NoSyn)) params)
       ||> Variable.restore_proper_fixes ctxt
-      ||> Proof_Context.set_mode Proof_Context.mode_schematic;
+      ||> Config.get ctxt schematic ? Proof_Context.set_mode Proof_Context.mode_schematic;
     val paramTs = map #2 params;
 
 
@@ -225,7 +228,7 @@
     val (fixed, fixes_ctxt) = param_ctxt
       |> Proof_Context.read_vars fixes |-> Proof_Context.add_fixes;
 
-    val (inst_tvars, inst_vars) = read_insts fixes_ctxt mixed_insts thm;
+    val ((inst_tvars, inst_vars), inst_ctxt) = read_insts thm mixed_insts fixes_ctxt;
 
 
     (* lift and instantiate rule *)
@@ -238,14 +241,14 @@
         (Logic.incr_indexes (fixed, paramTs, inc) t);
 
     val inst_tvars' = inst_tvars
-      |> map (apply2 (Thm.ctyp_of fixes_ctxt o Logic.incr_tvar inc) o apfst TVar);
+      |> map (apply2 (Thm.ctyp_of inst_ctxt o Logic.incr_tvar inc) o apfst TVar);
     val inst_vars' = inst_vars
-      |> map (fn (v, t) => apply2 (Thm.cterm_of fixes_ctxt) (lift_var v, lift_term t));
+      |> map (fn (v, t) => apply2 (Thm.cterm_of inst_ctxt) (lift_var v, lift_term t));
 
     val thm' =
       Drule.instantiate_normalize (inst_tvars', inst_vars')
         (Thm.lift_rule cgoal thm)
-      |> singleton (Variable.export fixes_ctxt param_ctxt);
+      |> singleton (Variable.export inst_ctxt param_ctxt);
   in
     compose_tac param_ctxt (bires_flag, thm', Thm.nprems_of thm) i
   end) i st;

--- a/src/Pure/variable.ML	Tue Mar 24 18:10:56 2015 +0100
+++ b/src/Pure/variable.ML	Tue Mar 24 23:39:42 2015 +0100
@@ -6,9 +6,6 @@
 
 signature VARIABLE =
 sig
-  val is_body: Proof.context -> bool
-  val set_body: bool -> Proof.context -> Proof.context
-  val restore_body: Proof.context -> Proof.context -> Proof.context
   val names_of: Proof.context -> Name.context
   val binds_of: Proof.context -> (typ * term) Vartab.table
   val maxidx_of: Proof.context -> int
@@ -34,6 +31,9 @@
   val declare_const: string * string -> Proof.context -> Proof.context
   val next_bound: string * typ -> Proof.context -> term * Proof.context
   val revert_bounds: Proof.context -> term -> term
+  val is_body: Proof.context -> bool
+  val set_body: bool -> Proof.context -> Proof.context
+  val restore_body: Proof.context -> Proof.context -> Proof.context
   val improper_fixes: Proof.context -> Proof.context
   val restore_proper_fixes: Proof.context -> Proof.context -> Proof.context
   val is_improper: Proof.context -> string -> bool
@@ -52,15 +52,16 @@
   val add_fixes: string list -> Proof.context -> string list * Proof.context
   val add_fixes_direct: string list -> Proof.context -> Proof.context
   val auto_fixes: term -> Proof.context -> Proof.context
+  val fix_dummy_patterns: term -> Proof.context -> term * Proof.context
   val variant_fixes: string list -> Proof.context -> string list * Proof.context
   val dest_fixes: Proof.context -> (string * string) list
-  val invent_types: sort list -> Proof.context -> (string * sort) list * Proof.context
   val export_terms: Proof.context -> Proof.context -> term list -> term list
   val exportT_terms: Proof.context -> Proof.context -> term list -> term list
   val exportT: Proof.context -> Proof.context -> thm list -> thm list
   val export_prf: Proof.context -> Proof.context -> Proofterm.proof -> Proofterm.proof
   val export: Proof.context -> Proof.context -> thm list -> thm list
   val export_morphism: Proof.context -> Proof.context -> morphism
+  val invent_types: sort list -> Proof.context -> (string * sort) list * Proof.context
   val importT_inst: term list -> Proof.context -> ((indexname * sort) * typ) list * Proof.context
   val import_inst: bool -> term list -> Proof.context ->
     (((indexname * sort) * typ) list * ((indexname * typ) * term) list) * Proof.context
@@ -89,8 +90,7 @@
 val empty_fixes: fixes = Name_Space.empty_table Markup.fixedN;
 
 datatype data = Data of
- {is_body: bool,                        (*inner body mode*)
-  names: Name.context,                  (*type/term variable names*)
+ {names: Name.context,                  (*type/term variable names*)
   consts: string Symtab.table,          (*consts within the local scope*)
   bounds: int * ((string * typ) * string) list,  (*next index, internal name, type, external name*)
   fixes: fixes,                         (*term fixes -- global name space, intern ~> extern*)
@@ -102,13 +102,12 @@
     typ Vartab.table *                  (*type constraints*)
     sort Vartab.table};                 (*default sorts*)
 
-fun make_data
-    (is_body, names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints) =
-  Data {is_body = is_body, names = names, consts = consts, bounds = bounds, fixes = fixes,
-    binds = binds, type_occs = type_occs, maxidx = maxidx, sorts = sorts, constraints = constraints};
+fun make_data (names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints) =
+  Data {names = names, consts = consts, bounds = bounds, fixes = fixes, binds = binds,
+    type_occs = type_occs, maxidx = maxidx, sorts = sorts, constraints = constraints};
 
 val empty_data =
-  make_data (false, Name.context, Symtab.empty, (0, []), empty_fixes, Vartab.empty,
+  make_data (Name.context, Symtab.empty, (0, []), empty_fixes, Vartab.empty,
     Symtab.empty, ~1, [], (Vartab.empty, Vartab.empty));
 
 structure Data = Proof_Data
@@ -118,66 +117,47 @@
 );
 
 fun map_data f =
-  Data.map (fn
-      Data {is_body, names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints} =>
-    make_data
-      (f (is_body, names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints)));
+  Data.map (fn Data {names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints} =>
+    make_data (f (names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints)));
 
 fun map_names f =
-  map_data (fn
-      (is_body, names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints) =>
-    (is_body, f names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints));
+  map_data (fn (names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints) =>
+    (f names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints));
 
 fun map_consts f =
-  map_data (fn
-      (is_body, names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints) =>
-    (is_body, names, f consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints));
+  map_data (fn (names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints) =>
+    (names, f consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints));
 
 fun map_bounds f =
-  map_data (fn
-      (is_body, names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints) =>
-    (is_body, names, consts, f bounds, fixes, binds, type_occs, maxidx, sorts, constraints));
+  map_data (fn (names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints) =>
+    (names, consts, f bounds, fixes, binds, type_occs, maxidx, sorts, constraints));
 
 fun map_fixes f =
-  map_data (fn
-      (is_body, names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints) =>
-    (is_body, names, consts, bounds, f fixes, binds, type_occs, maxidx, sorts, constraints));
+  map_data (fn (names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints) =>
+    (names, consts, bounds, f fixes, binds, type_occs, maxidx, sorts, constraints));
 
 fun map_binds f =
-  map_data (fn
-      (is_body, names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints) =>
-    (is_body, names, consts, bounds, fixes, f binds, type_occs, maxidx, sorts, constraints));
+  map_data (fn (names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints) =>
+    (names, consts, bounds, fixes, f binds, type_occs, maxidx, sorts, constraints));
 
 fun map_type_occs f =
-  map_data (fn
-      (is_body, names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints) =>
-    (is_body, names, consts, bounds, fixes, binds, f type_occs, maxidx, sorts, constraints));
+  map_data (fn (names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints) =>
+    (names, consts, bounds, fixes, binds, f type_occs, maxidx, sorts, constraints));
 
 fun map_maxidx f =
-  map_data (fn
-      (is_body, names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints) =>
-    (is_body, names, consts, bounds, fixes, binds, type_occs, f maxidx, sorts, constraints));
+  map_data (fn (names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints) =>
+    (names, consts, bounds, fixes, binds, type_occs, f maxidx, sorts, constraints));
 
 fun map_sorts f =
-  map_data (fn
-      (is_body, names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints) =>
-    (is_body, names, consts, bounds, fixes, binds, type_occs, maxidx, f sorts, constraints));
+  map_data (fn (names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints) =>
+    (names, consts, bounds, fixes, binds, type_occs, maxidx, f sorts, constraints));
 
 fun map_constraints f =
-  map_data (fn
-      (is_body, names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints) =>
-    (is_body, names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, f constraints));
+  map_data (fn (names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints) =>
+    (names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, f constraints));
 
 fun rep_data ctxt = Data.get ctxt |> (fn Data rep => rep);
 
-val is_body = #is_body o rep_data;
-
-fun set_body b =
-  map_data (fn (_, names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints) =>
-    (b, names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints));
-
-fun restore_body ctxt = set_body (is_body ctxt);
-
 val names_of = #names o rep_data;
 val fixes_of = #fixes o rep_data;
 val fixes_space = Name_Space.space_of_table o fixes_of;
@@ -338,6 +318,16 @@
 
 (** fixes **)
 
+(* inner body mode *)
+
+val inner_body =
+  Config.bool (Config.declare ("inner_body", @{here}) (K (Config.Bool false)));
+
+fun is_body ctxt = Config.get ctxt inner_body;
+val set_body = Config.put inner_body;
+fun restore_body ctxt = set_body (is_body ctxt);
+
+
 (* proper mode *)
 
 val proper_fixes =
@@ -460,11 +450,21 @@
   |> not (is_body ctxt) ? add_fixes_direct (rev (add_free_names ctxt t []))
   |> declare_term t;
 
-fun invent_types Ss ctxt =
-  let
-    val tfrees = Name.invent (names_of ctxt) Name.aT (length Ss) ~~ Ss;
-    val ctxt' = fold (declare_constraints o Logic.mk_type o TFree) tfrees ctxt;
-  in (tfrees, ctxt') end;
+
+(* dummy patterns *)
+
+fun fix_dummy_patterns (Const ("Pure.dummy_pattern", T)) ctxt =
+      let val ([x], ctxt') = add_fixes [Name.uu_] ctxt
+      in (Free (x, T), ctxt') end
+  | fix_dummy_patterns (Abs (x, T, b)) ctxt =
+      let val (b', ctxt') = fix_dummy_patterns b ctxt
+      in (Abs (x, T, b'), ctxt') end
+  | fix_dummy_patterns (t $ u) ctxt =
+      let
+        val (t', ctxt') = fix_dummy_patterns t ctxt;
+        val (u', ctxt'') = fix_dummy_patterns u ctxt';
+      in (t' $ u', ctxt'') end
+  | fix_dummy_patterns a ctxt = (a, ctxt);
 
 
 
@@ -541,6 +541,12 @@
 
 (** import -- fix schematic type/term variables **)
 
+fun invent_types Ss ctxt =
+  let
+    val tfrees = Name.invent (names_of ctxt) Name.aT (length Ss) ~~ Ss;
+    val ctxt' = fold (declare_constraints o Logic.mk_type o TFree) tfrees ctxt;
+  in (tfrees, ctxt') end;
+
 fun importT_inst ts ctxt =
   let
     val tvars = rev (fold Term.add_tvars ts []);

--- a/src/Tools/Code/code_thingol.ML	Tue Mar 24 18:10:56 2015 +0100
+++ b/src/Tools/Code/code_thingol.ML	Tue Mar 24 23:39:42 2015 +0100
@@ -895,7 +895,7 @@
       (fn thy'' => not (Sign.declared_const thy'' c)) (Theory.parents_of thy');
     fun consts_of_select thy' = filter (belongs_here thy') (consts_of thy');
     fun read_const_expr str =
-      (case Syntax.parse_token ctxt (K NONE) (K Markup.empty) (SOME o Symbol_Pos.implode o #1) str of
+      (case Syntax.parse_input ctxt (K NONE) (K Markup.empty) (SOME o Symbol_Pos.implode o #1) str of
         SOME "_" => ([], consts_of thy)
       | SOME s =>
           if String.isSuffix "._" s
@@ -910,7 +910,7 @@
   let
     val (consts, consts_permissive) = read_const_exprs_internal ctxt const_exprs;
     val consts' = implemented_deps
-      (consts_program_permissive ((Proof_Context.theory_of ctxt)) consts_permissive);
+      (consts_program_permissive (Proof_Context.theory_of ctxt) consts_permissive);
   in union (op =) consts' consts end;
 
 

--- a/src/Tools/induct_tacs.ML	Tue Mar 24 18:10:56 2015 +0100
+++ b/src/Tools/induct_tacs.ML	Tue Mar 24 23:39:42 2015 +0100
@@ -6,8 +6,10 @@
 
 signature INDUCT_TACS =
 sig
-  val case_tac: Proof.context -> string -> int -> tactic
-  val case_rule_tac: Proof.context -> string -> thm -> int -> tactic
+  val case_tac: Proof.context -> string -> (binding * string option * mixfix) list ->
+    int -> tactic
+  val case_rule_tac: Proof.context -> string -> (binding * string option * mixfix) list ->
+    thm -> int -> tactic
   val induct_tac: Proof.context -> string option list list -> int -> tactic
   val induct_rules_tac: Proof.context -> string option list list -> thm list -> int -> tactic
 end
@@ -26,29 +28,35 @@
         quote (Syntax.string_of_term ctxt u) ^ Position.here pos);
   in (u, U) end;
 
-fun gen_case_tac ctxt0 s opt_rule i st =
+fun gen_case_tac ctxt s fixes opt_rule i st =
   let
-    val (_, ctxt) = Variable.focus_subgoal i st ctxt0;
     val rule =
       (case opt_rule of
         SOME rule => rule
       | NONE =>
-          (case Induct.find_casesT ctxt
-              (#2 (check_type ctxt (Proof_Context.read_term_schematic ctxt s,
-                Syntax.read_token_pos s))) of
-            rule :: _ => rule
-          | [] => @{thm case_split}));
+          let
+            val ctxt' = ctxt
+              |> Variable.focus_subgoal i st |> #2
+              |> Config.get ctxt Rule_Insts.schematic ?
+                  Proof_Context.set_mode Proof_Context.mode_schematic
+              |> Context_Position.set_visible false;
+            val t = Syntax.read_term ctxt' s;
+          in
+            (case Induct.find_casesT ctxt' (#2 (check_type ctxt' (t, Syntax.read_input_pos s))) of
+              rule :: _ => rule
+            | [] => @{thm case_split})
+          end);
     val _ = Method.trace ctxt [rule];
 
     val xi =
       (case Induct.vars_of (Thm.term_of (Thm.cprem_of rule 1)) of
         Var (xi, _) :: _ => xi
       | _ => raise THM ("Malformed cases rule", 0, [rule]));
-  in Rule_Insts.res_inst_tac ctxt [((xi, Position.none), s)] [] rule i st end
+  in Rule_Insts.res_inst_tac ctxt [((xi, Position.none), s)] fixes rule i st end
   handle THM _ => Seq.empty;
 
-fun case_tac ctxt s = gen_case_tac ctxt s NONE;
-fun case_rule_tac ctxt s rule = gen_case_tac ctxt s (SOME rule);
+fun case_tac ctxt s xs = gen_case_tac ctxt s xs NONE;
+fun case_rule_tac ctxt s xs rule = gen_case_tac ctxt s xs (SOME rule);
 
 
 (* induction *)
@@ -72,7 +80,7 @@
     fun induct_var name =
       let
         val t = Syntax.read_term ctxt name;
-        val pos = Syntax.read_token_pos name;
+        val pos = Syntax.read_input_pos name;
         val (x, _) = Term.dest_Free t handle TERM _ =>
           error ("Induction argument not a variable: " ^
             quote (Syntax.string_of_term ctxt t) ^ Position.here pos);
@@ -130,8 +138,8 @@
 val _ =
   Theory.setup
    (Method.setup @{binding case_tac}
-      (Args.goal_spec -- Scan.lift Args.name_inner_syntax -- opt_rule >>
-        (fn ((quant, s), r) => fn ctxt => SIMPLE_METHOD'' quant (gen_case_tac ctxt s r)))
+      (Args.goal_spec -- Scan.lift (Args.name_inner_syntax -- Parse.for_fixes) -- opt_rule >>
+        (fn ((quant, (s, xs)), r) => fn ctxt => SIMPLE_METHOD'' quant (gen_case_tac ctxt s xs r)))
       "unstructured case analysis on types" #>
     Method.setup @{binding induct_tac}
       (Args.goal_spec -- varss -- opt_rules >>