# HG changeset patch
# User wenzelm
# Date 1427482265 -3600
# Node ID 04e569577c18884374ec998402dbdbf88aa62dc5
# Parent  442b09c0f898f302eb3125a8fe18d57c865b3ea6
proper Rule_Insts.read_term, e.g. to enable case_tac using "_";

diff -r 442b09c0f898 -r 04e569577c18 src/Pure/Tools/rule_insts.ML
--- a/src/Pure/Tools/rule_insts.ML	Fri Mar 27 17:46:08 2015 +0100
+++ b/src/Pure/Tools/rule_insts.ML	Fri Mar 27 19:51:05 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 read_term: string -> Proof.context -> term * Proof.context
   val schematic: bool Config.T
   val goal_context: int -> thm -> Proof.context -> (string * typ) list * Proof.context
   val res_inst_tac: Proof.context ->
@@ -70,6 +71,18 @@
     else error_var "Bad sort for instantiation of type variable: " (xi, pos)
   end;
 
+fun make_instT f v =
+  let
+    val T = TVar v;
+    val T' = f T;
+  in if T = T' then NONE else SOME (v, T') end;
+
+fun make_inst f v =
+  let
+    val t = Var v;
+    val t' = f t;
+  in if t aconv t' then NONE else SOME (v, t') end;
+
 fun read_terms ss Ts ctxt =
   let
     fun parse T = if T = propT then Syntax.parse_prop ctxt else Syntax.parse_term ctxt;
@@ -83,19 +96,13 @@
     val tyenv' = Vartab.fold (fn (xi, (S, T)) => cons ((xi, S), T)) tyenv [];
   in ((ts', tyenv'), ctxt') end;
 
-fun make_instT f v =
-  let
-    val T = TVar v;
-    val T' = f T;
-  in if T = T' then NONE else SOME (v, T') end;
+in
 
-fun make_inst f v =
+fun read_term s ctxt =
   let
-    val t = Var v;
-    val t' = f t;
-  in if t aconv t' then NONE else SOME (v, t') end;
-
-in
+    val (t, ctxt') = Variable.fix_dummy_patterns (Syntax.parse_term ctxt s) ctxt;
+    val t' = Syntax.check_term ctxt' t;
+  in (t', ctxt') end;
 
 fun read_insts thm mixed_insts ctxt =
   let
diff -r 442b09c0f898 -r 04e569577c18 src/Tools/induct_tacs.ML
--- a/src/Tools/induct_tacs.ML	Fri Mar 27 17:46:08 2015 +0100
+++ b/src/Tools/induct_tacs.ML	Fri Mar 27 19:51:05 2015 +0100
@@ -33,14 +33,13 @@
         SOME rule => rule
       | NONE =>
           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;
+            val (t, ctxt') = ctxt
+              |> Rule_Insts.goal_context i st |> #2
+              |> Context_Position.set_visible false
+              |> Rule_Insts.read_term s;
+            val pos = Syntax.read_input_pos s;
           in
-            (case Induct.find_casesT ctxt' (#2 (check_type ctxt' (t, Syntax.read_input_pos s))) of
+            (case Induct.find_casesT ctxt' (#2 (check_type ctxt' (t, pos))) of
               rule :: _ => rule
             | [] => @{thm case_split})
           end);