src/HOL/simpdata.ML
changeset 18708 4b3dadb4fe33
parent 18529 540da2415751
child 19472 896eb8056e97
     1.1 --- a/src/HOL/simpdata.ML	Thu Jan 19 15:45:10 2006 +0100
     1.2 +++ b/src/HOL/simpdata.ML	Thu Jan 19 21:22:08 2006 +0100
     1.3 @@ -425,7 +425,7 @@
     1.4  
     1.5  (* default simpset *)
     1.6  val simpsetup =
     1.7 -  [fn thy => (change_simpset_of thy (fn _ => HOL_ss addcongs [if_weak_cong]); thy)];
     1.8 +  (fn thy => (change_simpset_of thy (fn _ => HOL_ss addcongs [if_weak_cong]); thy));
     1.9  
    1.10  
    1.11  (*** integration of simplifier with classical reasoner ***)