src/FOL/simpdata.ML
changeset 54998 8601434fa334
parent 51717 9e7d1c139569
child 56245 84fc7dfa3cd4
     1.1 --- a/src/FOL/simpdata.ML	Sun Jan 12 13:16:00 2014 +0100
     1.2 +++ b/src/FOL/simpdata.ML	Sun Jan 12 14:32:22 2014 +0100
     1.3 @@ -123,7 +123,7 @@
     1.4    |> Simplifier.set_mkcong mk_meta_cong
     1.5    |> simpset_of;
     1.6  
     1.7 -fun unfold_tac ths ctxt =
     1.8 +fun unfold_tac ctxt ths =
     1.9    ALLGOALS (full_simp_tac (clear_simpset (put_simpset FOL_basic_ss ctxt) addsimps ths));
    1.10  
    1.11