src/HOL/Tools/Meson/meson.ML
changeset 46093 4bf24b90703c
parent 46071 1613933e412c
child 46503 186f4cab2ba0
--- a/src/HOL/Tools/Meson/meson.ML	Tue Jan 03 18:33:18 2012 +0100
+++ b/src/HOL/Tools/Meson/meson.ML	Tue Jan 03 18:33:18 2012 +0100
@@ -18,8 +18,8 @@
     thm list -> thm -> Proof.context
     -> Proof.context -> thm list * Proof.context
   val finish_cnf: thm list -> thm list
-  val presimplified_consts : Proof.context -> string list
-  val presimplify: Proof.context -> thm -> thm
+  val presimplified_consts : string list
+  val presimplify: thm -> thm
   val make_nnf: Proof.context -> thm -> thm
   val choice_theorems : theory -> thm list
   val skolemize_with_choice_theorems : Proof.context -> thm list -> thm -> thm
@@ -578,18 +578,18 @@
     addsimprocs [@{simproc defined_All}, @{simproc defined_Ex}, @{simproc neq},
                  @{simproc let_simp}]
 
-fun presimplified_consts ctxt =
+val presimplified_consts =
   [@{const_name simp_implies}, @{const_name False}, @{const_name True},
    @{const_name Ex1}, @{const_name Ball}, @{const_name Bex}, @{const_name If},
    @{const_name Let}]
 
-fun presimplify ctxt =
+val presimplify =
   rewrite_rule (map safe_mk_meta_eq nnf_simps)
   #> simplify nnf_ss
   #> Raw_Simplifier.rewrite_rule @{thms Let_def_raw}
 
 fun make_nnf ctxt th = case prems_of th of
-    [] => th |> presimplify ctxt |> make_nnf1 ctxt
+    [] => th |> presimplify |> make_nnf1 ctxt
   | _ => raise THM ("make_nnf: premises in argument", 0, [th]);
 
 fun choice_theorems thy =