# HG changeset patch # User wenzelm # Date 1346235501 -7200 # Node ID 0e1cab4a334e9682a90fa23ff80b0af138a9fd47 # Parent c84278efa9d5073d15fce3a5ddb01acbc10dcfe3 more precise indentation; diff -r c84278efa9d5 -r 0e1cab4a334e src/HOL/Tools/Function/function.ML --- a/src/HOL/Tools/Function/function.ML Wed Aug 29 12:07:57 2012 +0200 +++ b/src/HOL/Tools/Function/function.ML Wed Aug 29 12:18:21 2012 +0200 @@ -167,46 +167,46 @@ fun prepare_termination_proof prep_term raw_term_opt lthy = let val term_opt = Option.map (prep_term lthy) raw_term_opt - val info = the (case term_opt of - SOME t => (import_function_data t lthy - handle Option.Option => - error ("Not a function: " ^ quote (Syntax.string_of_term lthy t))) - | NONE => (import_last_function lthy handle Option.Option => error "Not a function")) + val info = + the (case term_opt of + SOME t => (import_function_data t lthy + handle Option.Option => + error ("Not a function: " ^ quote (Syntax.string_of_term lthy t))) + | NONE => (import_last_function lthy handle Option.Option => error "Not a function")) - val { termination, fs, R, add_simps, case_names, psimps, - pinducts, defname, ...} = info - val domT = domain_type (fastype_of R) - val goal = HOLogic.mk_Trueprop - (HOLogic.mk_all ("x", domT, mk_acc domT R $ Free ("x", domT))) - fun afterqed [[totality]] lthy = - let - val totality = Thm.close_derivation totality - val remove_domain_condition = - full_simplify (HOL_basic_ss addsimps [totality, @{thm True_implies_equals}]) - val tsimps = map remove_domain_condition psimps - val tinduct = map remove_domain_condition pinducts + val { termination, fs, R, add_simps, case_names, psimps, + pinducts, defname, ...} = info + val domT = domain_type (fastype_of R) + val goal = HOLogic.mk_Trueprop (HOLogic.mk_all ("x", domT, mk_acc domT R $ Free ("x", domT))) + fun afterqed [[totality]] lthy = + let + val totality = Thm.close_derivation totality + val remove_domain_condition = + full_simplify (HOL_basic_ss addsimps [totality, @{thm True_implies_equals}]) + val tsimps = map remove_domain_condition psimps + val tinduct = map remove_domain_condition pinducts - fun qualify n = Binding.name n - |> Binding.qualify true defname - in - lthy - |> add_simps I "simps" I simp_attribs tsimps - ||>> Local_Theory.note - ((qualify "induct", - [Attrib.internal (K (Rule_Cases.case_names case_names))]), - tinduct) - |-> (fn (simps, (_, inducts)) => fn lthy => - let val info' = { is_partial=false, defname=defname, add_simps=add_simps, - case_names=case_names, fs=fs, R=R, psimps=psimps, pinducts=pinducts, - simps=SOME simps, inducts=SOME inducts, termination=termination } - in - (info', - lthy - |> Local_Theory.declaration {syntax = false, pervasive = false} - (add_function_data o transform_function_data info') - |> Spec_Rules.add Spec_Rules.Equational (fs, tsimps)) - end) - end + fun qualify n = Binding.name n + |> Binding.qualify true defname + in + lthy + |> add_simps I "simps" I simp_attribs tsimps + ||>> Local_Theory.note + ((qualify "induct", + [Attrib.internal (K (Rule_Cases.case_names case_names))]), + tinduct) + |-> (fn (simps, (_, inducts)) => fn lthy => + let val info' = { is_partial=false, defname=defname, add_simps=add_simps, + case_names=case_names, fs=fs, R=R, psimps=psimps, pinducts=pinducts, + simps=SOME simps, inducts=SOME inducts, termination=termination } + in + (info', + lthy + |> Local_Theory.declaration {syntax = false, pervasive = false} + (add_function_data o transform_function_data info') + |> Spec_Rules.add Spec_Rules.Equational (fs, tsimps)) + end) + end in (goal, afterqed, termination) end