changeset 49586 | d5e342ffe91e |
parent 49585 | 5c4a12550491 |
child 49630 | 9f6ca87ab405 |
--- a/src/HOL/BNF/Tools/bnf_comp.ML Wed Sep 26 10:00:59 2012 +0200 +++ b/src/HOL/BNF/Tools/bnf_comp.ML Wed Sep 26 10:00:59 2012 +0200 @@ -167,7 +167,7 @@ |> sort (rev_order o int_ord o pairself fst) |> map snd) @ [map_id_of_bnf outer]; in - (EVERY' (map (fn thm => subst_tac ctxt [thm]) thms) THEN' rtac refl) 1 + (EVERY' (map (fn thm => subst_tac ctxt NONE [thm]) thms) THEN' rtac refl) 1 end; fun map_comp_tac _ =