# HG changeset patch
# User oheimb
# Date 879334483 -3600
# Node ID 688050e83d890fa81aea282bfc1347003aba7f55
# Parent  96632970d20361dbd73d068cdea6a6001be6fdd0
restored last version

diff -r 96632970d203 -r 688050e83d89 src/HOL/cladata.ML
--- a/src/HOL/cladata.ML	Wed Nov 12 12:30:15 1997 +0100
+++ b/src/HOL/cladata.ML	Wed Nov 12 12:34:43 1997 +0100
@@ -26,9 +26,6 @@
 structure Hypsubst = HypsubstFun(Hypsubst_Data);
 open Hypsubst;
 
-val thin_refl = prove_goal HOL.thy 
-	"!!X. [|x=x; PROP W|] ==> PROP W" (K [atac 1]);
-
 (*** Applying ClassicalFun to create a classical prover ***)
 structure Classical_Data = 
   struct
@@ -36,8 +33,7 @@
   val mp        = mp
   val not_elim  = notE
   val classical = classical
-  val thin_refl = thin_refl
-  val hyp_subst_tacs= [REPEAT_DETERM o ematch_tac [thin_refl] THEN' hyp_subst_tac]
+  val hyp_subst_tacs=[hyp_subst_tac]
   end;
 
 structure Classical = ClassicalFun(Classical_Data);