src/Provers/simplifier.ML

   val setmksimps: simpset * (thm -> thm list) -> simpset
   val setsubgoaler: simpset * (simpset -> int -> tactic) -> simpset
   val simp_tac: simpset -> int -> tactic
 end;
 
-structure Simplifier:SIMPLIFIER =
+functor SimplifierFUN():SIMPLIFIER =
 struct
 
 datatype simpset =
   SS of {mss: meta_simpset,
          simps: thm list,

 val asm_full_simp_tac = gen_simp_tac (true,true);
 val asm_simp_tac = gen_simp_tac (false,true);
 val simp_tac = gen_simp_tac (false,false);
 
 end;
+
+structure Simplifier = SimplifierFUN();