--- 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);