changeset 54883 | dd04a8b654fc |
parent 54401 | f6950854855d |
child 55997 | 9dc5ce83202c |
--- a/src/HOL/Library/simps_case_conv.ML Tue Dec 31 11:19:14 2013 +0100 +++ b/src/HOL/Library/simps_case_conv.ML Tue Dec 31 14:29:16 2013 +0100 @@ -143,7 +143,7 @@ tac ctxt {splits=split_thms, intros=ths, defs=def_thms}) in th |> singleton (Proof_Context.export ctxt3 ctxt) - |> Goal.norm_result + |> Goal.norm_result ctxt end end