src/HOL/Tools/Sledgehammer/metis_tactics.ML

 
 (* ------------------------------------------------------------------------- *)
 (* Useful Theorems                                                           *)
 (* ------------------------------------------------------------------------- *)
 val EXCLUDED_MIDDLE = @{lemma "P ==> ~ P ==> False" by (rule notE)}
-val REFL_THM = incr_indexes 2 @{lemma "t ~= t ==> False" by simp}
+val REFL_THM = Thm.incr_indexes 2 @{lemma "t ~= t ==> False" by simp}
 val subst_em = @{lemma "s = t ==> P s ==> ~ P t ==> False" by simp}
 val ssubst_em = @{lemma "s = t ==> P t ==> ~ P s ==> False" by simp}
 
 (* ------------------------------------------------------------------------- *)
 (* Useful Functions                                                          *)

       val [vx] = Term.add_vars (prop_of th) []
       val substs = [(cterm_of thy (Var vx), cterm_of thy i_atm)]
   in  cterm_instantiate substs th  end;
 
 (* INFERENCE RULE: AXIOM *)
-fun axiom_inf thpairs th = incr_indexes 1 (lookth thpairs th);
+fun axiom_inf thpairs th = Thm.incr_indexes 1 (lookth thpairs th);
     (*This causes variables to have an index of 1 by default. SEE ALSO mk_var above.*)
 
 (* INFERENCE RULE: ASSUME *)
 fun assume_inf ctxt mode atm =
   inst_excluded_middle

       val tm_abs = Term.Abs("x", Term.type_of tm_subst, body)
       val _ = trace_msg (fn () => "abstraction: " ^ Syntax.string_of_term ctxt tm_abs)
       val _ = trace_msg (fn () => "i_tm: " ^ Syntax.string_of_term ctxt i_tm)
       val _ = trace_msg (fn () => "located term: " ^ Syntax.string_of_term ctxt tm_subst)
       val imax = maxidx_of_term (i_tm $ tm_abs $ tm_subst)  (*ill typed but gives right max*)
-      val subst' = incr_indexes (imax+1) (if pos then subst_em else ssubst_em)
+      val subst' = Thm.incr_indexes (imax+1) (if pos then subst_em else ssubst_em)
       val _ = trace_msg (fn () => "subst' " ^ Display.string_of_thm ctxt subst')
       val eq_terms = map (pairself (cterm_of thy))
         (ListPair.zip (OldTerm.term_vars (prop_of subst'), [tm_abs, tm_subst, i_tm]))
   in  cterm_instantiate eq_terms subst'  end;