--- a/src/LCF/LCF.thy Thu Mar 19 17:25:57 2015 +0100
+++ b/src/LCF/LCF.thy Thu Mar 19 22:30:57 2015 +0100
@@ -321,7 +321,7 @@
method_setup induct = {*
Scan.lift Args.name_inner_syntax >> (fn v => fn ctxt =>
SIMPLE_METHOD' (fn i =>
- res_inst_tac ctxt [(("f", 0), v)] @{thm induct} i THEN
+ res_inst_tac ctxt [((("f", 0), Position.none), v)] @{thm induct} i THEN
REPEAT (resolve_tac ctxt @{thms adm_lemmas} i)))
*}
@@ -380,7 +380,8 @@
ML {*
fun induct2_tac ctxt (f, g) i =
- res_inst_tac ctxt [(("f", 0), f), (("g", 0), g)] @{thm induct2} i THEN
+ res_inst_tac ctxt
+ [((("f", 0), Position.none), f), ((("g", 0), Position.none), g)] @{thm induct2} i THEN
REPEAT(resolve_tac ctxt @{thms adm_lemmas} i)
*}