--- a/src/HOL/Library/State_Monad.thy Wed Dec 13 20:38:18 2006 +0100
+++ b/src/HOL/Library/State_Monad.thy Wed Dec 13 20:38:19 2006 +0100
@@ -78,10 +78,6 @@
run :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" where
"run f = f"
-print_ast_translation {*[
- (Sign.const_syntax_name (the_context ()) "State_Monad.run", fn (f::ts) => Syntax.mk_appl f ts)
-]*}
-
syntax (xsymbols)
mbind :: "('a \<Rightarrow> 'b \<times> 'c) \<Rightarrow> ('b \<Rightarrow> 'c \<Rightarrow> 'd) \<Rightarrow> 'a \<Rightarrow> 'd"
(infixl "\<guillemotright>=" 60)
@@ -91,6 +87,10 @@
abbreviation (input)
"return \<equiv> Pair"
+print_ast_translation {*[
+ (Sign.const_syntax_name (the_context ()) "State_Monad.run", fn (f::ts) => Syntax.mk_appl f ts)
+]*}
+
text {*
Given two transformations @{term f} and @{term g}, they
may be directly composed using the @{term "op \<guillemotright>"} combinator,
--- a/src/HOL/Tools/function_package/fundef_common.ML Wed Dec 13 20:38:18 2006 +0100
+++ b/src/HOL/Tools/function_package/fundef_common.ML Wed Dec 13 20:38:19 2006 +0100
@@ -249,7 +249,7 @@
fun print _ _ = ()
end);
-val get_termination_rule = TerminationRule.get
+val get_termination_rule = TerminationRule.get
val set_termination_rule = TerminationRule.map o K o SOME
--- a/src/Pure/Tools/codegen_data.ML Wed Dec 13 20:38:18 2006 +0100
+++ b/src/Pure/Tools/codegen_data.ML Wed Dec 13 20:38:19 2006 +0100
@@ -739,7 +739,7 @@
|> fold (fn (_, f) => apply_preproc thy f) ((#preprocs o the_preproc o get_exec) thy)
|> map (rewrite_func ((#inlines o the_preproc o get_exec) thy))
|> fold (fn (_, f) => apply_inline_proc thy f) ((#inline_procs o the_preproc o get_exec) thy)
-(*FIXME - must check: rewrite rule, function equation, proper constant |> map (snd o check_func false thy) *)
+(*FIXME - must check: rewrite rule, function equation, proper constant |> map (snd o check_func false thy) *)
|> sort (cmp_thms thy)
|> common_typ_funcs thy;