src/HOL/Tools/simpdata.ML
changeset 36543 0e7fc5bf38de
parent 35364 b8c62d60195c
child 36603 d5d6111761a6
--- a/src/HOL/Tools/simpdata.ML	Thu Apr 29 22:08:57 2010 +0200
+++ b/src/HOL/Tools/simpdata.ML	Thu Apr 29 22:56:32 2010 +0200
@@ -48,7 +48,7 @@
    | _ $ (Const (@{const_name "Not"}, _) $ _) => th RS @{thm Eq_FalseI}
    | _ => th RS @{thm Eq_TrueI}
 
-fun mk_eq_True r =
+fun mk_eq_True (_: simpset) r =
   SOME (r RS @{thm meta_eq_to_obj_eq} RS @{thm Eq_TrueI}) handle Thm.THM _ => NONE;
 
 (* Produce theorems of the form
@@ -80,7 +80,7 @@
   end;
 
 (*Congruence rules for = (instead of ==)*)
-fun mk_meta_cong rl = zero_var_indexes
+fun mk_meta_cong (_: simpset) rl = zero_var_indexes
   (let val rl' = Seq.hd (TRYALL (fn i => fn st =>
      rtac (lift_meta_eq_to_obj_eq i st) i st) rl)
    in mk_meta_eq rl' handle THM _ =>
@@ -107,7 +107,7 @@
       end;
   in atoms end;
 
-fun mksimps pairs =
+fun mksimps pairs (_: simpset) =
   map_filter (try mk_eq) o mk_atomize pairs o gen_all;
 
 fun unsafe_solver_tac prems =