Removed dead code in function mk_deftab.
authorberghofe
Mon, 19 Oct 2009 16:47:21 +0200
changeset 33001 82382652e5e7
parent 33000 d31a52dbe91e
child 33002 f3f02f36a3e2
child 33008 b0ff69f0a248
Removed dead code in function mk_deftab.
src/Pure/codegen.ML
--- a/src/Pure/codegen.ML	Mon Oct 19 16:45:52 2009 +0200
+++ b/src/Pure/codegen.ML	Mon Oct 19 16:47:21 2009 +0200
@@ -500,8 +500,6 @@
   let
     val axmss = map (fn thy' => (Context.theory_name thy', Theory.axiom_table thy'))
       (thy :: Theory.ancestors_of thy);
-    fun prep_def def = (case preprocess thy [def] of
-      [def'] => prop_of def' | _ => error "mk_deftab: bad preprocessor");
     fun add_def thyname (name, t) = (case dest_prim_def t of
         NONE => I
       | SOME (s, (T, _)) => Symtab.map_default (s, [])