changeset 17956 | 369e2af8ee45 |
parent 17906 | 719364f5179b |
child 18049 | 156bba334c12 |
--- a/src/HOL/List.thy Fri Oct 21 18:14:32 2005 +0200 +++ b/src/HOL/List.thy Fri Oct 21 18:14:34 2005 +0200 @@ -453,7 +453,7 @@ val app = Const("List.op @",appT) val F2 = eq $ (app$lhs1$lastl) $ (app$rhs1$lastr) val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (F,F2)); - val thm = Tactic.prove sg [] [] eq + val thm = Goal.prove sg [] [] eq (K (simp_tac (Simplifier.inherit_context ss rearr_ss) 1)); in SOME ((conv RS (thm RS trans)) RS eq_reflection) end;