whitespace correction
authorhaftmann
Wed Dec 13 20:38:19 2006 +0100 (2006-12-13)
changeset 2183584fd5de0691c
parent 21834 770ce948a59b
child 21836 b2cbcf8a018e
whitespace correction
src/HOL/Library/State_Monad.thy
src/HOL/Tools/function_package/fundef_common.ML
src/Pure/Tools/codegen_data.ML
     1.1 --- a/src/HOL/Library/State_Monad.thy	Wed Dec 13 20:38:18 2006 +0100
     1.2 +++ b/src/HOL/Library/State_Monad.thy	Wed Dec 13 20:38:19 2006 +0100
     1.3 @@ -78,10 +78,6 @@
     1.4    run :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" where
     1.5    "run f = f"
     1.6  
     1.7 -print_ast_translation {*[
     1.8 -  (Sign.const_syntax_name (the_context ()) "State_Monad.run", fn (f::ts) => Syntax.mk_appl f ts)
     1.9 -]*}
    1.10 -
    1.11  syntax (xsymbols)
    1.12    mbind :: "('a \<Rightarrow> 'b \<times> 'c) \<Rightarrow> ('b \<Rightarrow> 'c \<Rightarrow> 'd) \<Rightarrow> 'a \<Rightarrow> 'd"
    1.13      (infixl "\<guillemotright>=" 60)
    1.14 @@ -91,6 +87,10 @@
    1.15  abbreviation (input)
    1.16    "return \<equiv> Pair"
    1.17  
    1.18 +print_ast_translation {*[
    1.19 +  (Sign.const_syntax_name (the_context ()) "State_Monad.run", fn (f::ts) => Syntax.mk_appl f ts)
    1.20 +]*}
    1.21 +
    1.22  text {*
    1.23    Given two transformations @{term f} and @{term g}, they
    1.24    may be directly composed using the @{term "op \<guillemotright>"} combinator,
     2.1 --- a/src/HOL/Tools/function_package/fundef_common.ML	Wed Dec 13 20:38:18 2006 +0100
     2.2 +++ b/src/HOL/Tools/function_package/fundef_common.ML	Wed Dec 13 20:38:19 2006 +0100
     2.3 @@ -249,7 +249,7 @@
     2.4      fun print  _ _ = ()
     2.5  end);
     2.6  
     2.7 -val get_termination_rule = TerminationRule.get 
     2.8 +val get_termination_rule = TerminationRule.get
     2.9  val set_termination_rule = TerminationRule.map o K o SOME
    2.10  
    2.11  
     3.1 --- a/src/Pure/Tools/codegen_data.ML	Wed Dec 13 20:38:18 2006 +0100
     3.2 +++ b/src/Pure/Tools/codegen_data.ML	Wed Dec 13 20:38:19 2006 +0100
     3.3 @@ -739,7 +739,7 @@
     3.4    |> fold (fn (_, f) => apply_preproc thy f) ((#preprocs o the_preproc o get_exec) thy)
     3.5    |> map (rewrite_func ((#inlines o the_preproc o get_exec) thy))
     3.6    |> fold (fn (_, f) => apply_inline_proc thy f) ((#inline_procs o the_preproc o get_exec) thy)
     3.7 -(*FIXME - must check: rewrite rule, function equation, proper constant |> map (snd o check_func false thy)  *)
     3.8 +(*FIXME - must check: rewrite rule, function equation, proper constant |> map (snd o check_func false thy) *)
     3.9    |> sort (cmp_thms thy)
    3.10    |> common_typ_funcs thy;
    3.11