tuned

--- a/src/HOL/HOL.thy	Sat Nov 18 00:20:16 2006 +0100
+++ b/src/HOL/HOL.thy	Sat Nov 18 00:20:17 2006 +0100
@@ -208,11 +208,11 @@
 
 typed_print_translation {*
 let
-  val syntax_name = Sign.const_syntax_name (the_context ());
+  val thy = the_context ();
   fun tr' c = (c, fn show_sorts => fn T => fn ts =>
     if T = dummyT orelse not (! show_types) andalso can Term.dest_Type T then raise Match
     else Syntax.const Syntax.constrainC $ Syntax.const c $ Syntax.term_of_typ show_sorts T);
-in map (tr' o Sign.const_syntax_name (the_context ())) ["HOL.one", "HOL.zero"] end;
+in map (tr' o Sign.const_syntax_name thy) ["HOL.one", "HOL.zero"] end;
 *} -- {* show types that are presumably too general *}
 
 notation

--- a/src/HOL/Tools/recfun_codegen.ML	Sat Nov 18 00:20:16 2006 +0100
+++ b/src/HOL/Tools/recfun_codegen.ML	Sat Nov 18 00:20:17 2006 +0100
@@ -36,7 +36,7 @@
 fun warn thm = warning ("RecfunCodegen: Not a proper equation:\n" ^
   string_of_thm thm);
 
-fun add optmod = Thm.declaration_attribute (fn thm => Context.mapping
+fun add optmod =
   let
     fun add thm =
       if Pattern.pattern (lhs_of thm) then
@@ -45,9 +45,9 @@
       else tap (fn _ => warn thm)
       handle TERM _ => tap (fn _ => warn thm);
   in
-    add thm
-    #> CodegenData.add_func_legacy thm
-  end I);
+    Thm.declaration_attribute (fn thm => Context.mapping
+      (add thm #> CodegenData.add_func_legacy thm) I)
+  end;
 
 fun del_thm thm thy =
   let
@@ -103,7 +103,7 @@
     val (s, T) = const_of (hd eqs);
 
     fun mk_fundef module fname prfx gr [] = (gr, [])
-      | mk_fundef module fname prfx gr ((fname', (lhs, rhs)) :: xs) =
+      | mk_fundef module fname prfx gr ((fname' : string, (lhs, rhs)) :: xs) =
       let
         val (gr1, pl) = invoke_codegen thy defs dname module false (gr, lhs);
         val (gr2, pr) = invoke_codegen thy defs dname module false (gr1, rhs);