--- a/src/Pure/simplifier.ML Mon Apr 23 20:44:08 2007 +0200
+++ b/src/Pure/simplifier.ML Mon Apr 23 20:44:09 2007 +0200
@@ -213,14 +213,6 @@
local
-(* FIXME *)
-fun read_terms ctxt ts =
- #1 (ProofContext.read_termTs ctxt (K false) (K NONE) (K NONE) []
- (map (rpair dummyT) ts));
-
-(* FIXME *)
-fun cert_terms ctxt ts = map (ProofContext.cert_term ctxt) ts;
-
fun gen_simproc prep {name, lhss, proc, identifier} lthy =
let
val naming = LocalTheory.full_naming lthy;
@@ -253,8 +245,8 @@
in
-val def_simproc = gen_simproc read_terms;
-val def_simproc_i = gen_simproc cert_terms;
+val def_simproc = gen_simproc ProofContext.read_terms;
+val def_simproc_i = gen_simproc ProofContext.cert_terms;
end;