changeset 17956 | 369e2af8ee45 |
parent 17877 | 67d5ab1cb0d8 |
child 20044 | 92cc2f4c7335 |
--- a/src/HOL/Algebra/abstract/Ring.thy Fri Oct 21 18:14:32 2005 +0200 +++ b/src/HOL/Algebra/abstract/Ring.thy Fri Oct 21 18:14:34 2005 +0200 @@ -164,7 +164,7 @@ "t * u::'a::ring", "- t::'a::ring"]; fun proc sg ss t = - let val rew = Tactic.prove sg [] [] + let val rew = Goal.prove sg [] [] (HOLogic.mk_Trueprop (HOLogic.mk_eq (t, Var (("x", Term.maxidx_of_term t + 1), fastype_of t)))) (fn _ => simp_tac (Simplifier.inherit_context ss ring_ss) 1)