# HG changeset patch
# User oheimb
# Date 934817068 -7200
# Node ID 08a354bbc34ccdc99a2373307df59fe14db10765
# Parent  1ad29e7d917bb9460bb665f0c166441c27ef8eff
re-added refl in safe_solver

diff -r 1ad29e7d917b -r 08a354bbc34c src/HOL/simpdata.ML
--- a/src/HOL/simpdata.ML	Mon Aug 16 16:44:47 1999 +0200
+++ b/src/HOL/simpdata.ML	Mon Aug 16 17:24:28 1999 +0200
@@ -429,10 +429,10 @@
 
 fun mksimps pairs = (map mk_eq o mk_atomize pairs o gen_all);
 
-fun unsafe_solver prems = FIRST'[resolve_tac (reflexive_thm::TrueI::refl::prems),
-				 atac, etac FalseE];
+fun unsafe_solver prems = FIRST'[resolve_tac(reflexive_thm::TrueI::refl::prems),
+				 atac         ,       etac  FalseE ];
 (*No premature instantiation of variables during simplification*)
-fun   safe_solver prems = FIRST'[match_tac (reflexive_thm::TrueI::prems),
+fun   safe_solver prems = FIRST'[  match_tac(reflexive_thm::TrueI::refl::prems),
 				 eq_assume_tac, ematch_tac [FalseE]];
 
 val HOL_basic_ss = empty_ss setsubgoaler asm_simp_tac