# HG changeset patch
# User haftmann
# Date 1166038699 -3600
# Node ID 84fd5de0691c02fc9b657272f4bb164c78bcfba9
# Parent  770ce948a59b5700fc566a9727b198603d254ef9
whitespace correction

diff -r 770ce948a59b -r 84fd5de0691c src/HOL/Library/State_Monad.thy
--- 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,
diff -r 770ce948a59b -r 84fd5de0691c src/HOL/Tools/function_package/fundef_common.ML
--- 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
 
 
diff -r 770ce948a59b -r 84fd5de0691c src/Pure/Tools/codegen_data.ML
--- 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;