# HG changeset patch
# User wenzelm
# Date 1152654572 -7200
# Node ID 26747ea32d35e339ce1b4fc3d8e4d06268e412c8
# Parent  6676a17dfc88c521656584319ab3eb1e32f00527
avoid reference to internal skolem;

diff -r 6676a17dfc88 -r 26747ea32d35 src/HOL/Bali/AxCompl.thy
--- a/src/HOL/Bali/AxCompl.thy	Tue Jul 11 23:00:39 2006 +0200
+++ b/src/HOL/Bali/AxCompl.thy	Tue Jul 11 23:49:32 2006 +0200
@@ -1159,7 +1159,7 @@
 	apply (rule ax_derivs.BinOp)
 	apply  (erule MGFnD [THEN ax_NormalD])
 	apply (rule allI)
-	apply (case_tac "need_second_arg binop__ v1")
+	apply (case_tac "need_second_arg binop v1")
 	apply  simp
 	apply  (erule MGFnD' [THEN conseq12])
 	apply  (fastsimp intro: eval.BinOp)