--- a/src/Tools/induct_tacs.ML Mon Mar 23 23:16:40 2015 +0100
+++ b/src/Tools/induct_tacs.ML Tue Mar 24 11:53:18 2015 +0100
@@ -35,7 +35,7 @@
| NONE =>
(case Induct.find_casesT ctxt
(#2 (check_type ctxt (Proof_Context.read_term_schematic ctxt s,
- Syntax.read_token_pos s))) of
+ Syntax.read_input_pos s))) of
rule :: _ => rule
| [] => @{thm case_split}));
val _ = Method.trace ctxt [rule];
@@ -72,7 +72,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);