# HG changeset patch
# User huffman
# Date 1232058818 28800
# Node ID 35c2654a95da72a98a915b1399fb84944780a325
# Parent  8858d197a9b6d00ba9f2747a3a33fa3e73f6ac8b
use match_tac instead of resolve_tac for continuity simproc

diff -r 8858d197a9b6 -r 35c2654a95da src/HOLCF/Cont.thy
--- a/src/HOLCF/Cont.thy	Thu Jan 15 12:43:41 2009 -0800
+++ b/src/HOLCF/Cont.thy	Thu Jan 15 14:33:38 2009 -0800
@@ -159,7 +159,7 @@
     let
       val tr = instantiate' [] [SOME (cterm_of thy t)] Eq_TrueI;
       val rules = Cont2ContData.get (Simplifier.the_context ss);
-      val tac = REPEAT_ALL_NEW (resolve_tac rules);
+      val tac = REPEAT_ALL_NEW (match_tac rules);
     in Option.map fst (Seq.pull (tac 1 tr)) end
 
   val proc =