diff -r 896eb8056e97 -r d87a8838afa4 src/Pure/codegen.ML
--- a/src/Pure/codegen.ML	Wed Apr 26 20:34:11 2006 +0200
+++ b/src/Pure/codegen.ML	Wed Apr 26 22:38:05 2006 +0200
@@ -516,12 +516,12 @@
 
 fun theory_of_type s thy =
   if Sign.declared_tyname thy s
-  then SOME (if_none (get_first (theory_of_type s) (Theory.parents_of thy)) thy)
+  then SOME (the_default thy (get_first (theory_of_type s) (Theory.parents_of thy)))
   else NONE;
 
 fun theory_of_const s thy =
   if Sign.declared_const thy s
-  then SOME (if_none (get_first (theory_of_const s) (Theory.parents_of thy)) thy)
+  then SOME (the_default thy (get_first (theory_of_const s) (Theory.parents_of thy)))
   else NONE;
 
 fun thyname_of_type s thy = (case theory_of_type s thy of
@@ -587,7 +587,7 @@
           NONE => defs
         | SOME (s, (T, (args, rhs))) => Symtab.update
             (s, (T, (thyname, split_last (rename_terms (args @ [rhs])))) ::
-            if_none (Symtab.lookup defs s) []) defs))
+            the_default [] (Symtab.lookup defs s)) defs))
   in
     foldl (fn ((thyname, axms), defs) =>
       Symtab.foldl (add_def thyname) (defs, axms)) Symtab.empty axmss