src/CCL/Wfd.thy
changeset 58957 c9e744ea8a38
parent 58889 5b7a9633cfa8
child 58963 26bf09b95dda
     1.1 --- a/src/CCL/Wfd.thy	Sun Nov 09 14:08:00 2014 +0100
     1.2 +++ b/src/CCL/Wfd.thy	Sun Nov 09 17:04:14 2014 +0100
     1.3 @@ -453,10 +453,11 @@
     1.4    in IHinst tac @{thms rcallTs} i end
     1.5    THEN eresolve_tac @{thms rcall_lemmas} i
     1.6  
     1.7 -fun raw_step_tac ctxt prems i = ares_tac (prems@type_rls) i ORELSE
     1.8 -                           rcall_tac ctxt i ORELSE
     1.9 -                           ematch_tac [@{thm SubtypeE}] i ORELSE
    1.10 -                           match_tac [@{thm SubtypeI}] i
    1.11 +fun raw_step_tac ctxt prems i =
    1.12 +  ares_tac (prems@type_rls) i ORELSE
    1.13 +  rcall_tac ctxt i ORELSE
    1.14 +  ematch_tac ctxt [@{thm SubtypeE}] i ORELSE
    1.15 +  match_tac ctxt [@{thm SubtypeI}] i
    1.16  
    1.17  fun tc_step_tac ctxt prems = SUBGOAL (fn (Bi,i) =>
    1.18            if is_rigid_prog Bi then raw_step_tac ctxt prems i else no_tac)