src/LCF/LCF.thy

   adm_not_eq_tr adm_conj adm_disj adm_imp adm_all
 
 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)))
 *}
 
 lemma least_FIX: "f(p) = p \<Longrightarrow> FIX(f) << p"
   apply (induct f)

   apply (rule 3)
   done
 
 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)
 *}
 
 end