clarified signature: proper result;
authorwenzelm
Mon Sep 11 18:36:13 2017 +0200 (21 months ago)
changeset 6665352bf9f67a3c9
parent 66652 93edcbc88536
child 66654 4a812abde314
clarified signature: proper result;
src/HOL/Tools/Function/partial_function.ML
     1.1 --- a/src/HOL/Tools/Function/partial_function.ML	Mon Sep 11 17:07:38 2017 +0100
     1.2 +++ b/src/HOL/Tools/Function/partial_function.ML	Mon Sep 11 18:36:13 2017 +0200
     1.3 @@ -9,9 +9,9 @@
     1.4    val init: string -> term -> term -> thm -> thm -> thm option -> declaration
     1.5    val mono_tac: Proof.context -> int -> tactic
     1.6    val add_partial_function: string -> (binding * typ option * mixfix) list ->
     1.7 -    Attrib.binding * term -> local_theory -> local_theory
     1.8 +    Attrib.binding * term -> local_theory -> (term * thm) * local_theory
     1.9    val add_partial_function_cmd: string -> (binding * string option * mixfix) list ->
    1.10 -    Attrib.binding * string -> local_theory -> local_theory
    1.11 +    Attrib.binding * string -> local_theory -> (term * thm) * local_theory
    1.12  end;
    1.13  
    1.14  structure Partial_Function: PARTIAL_FUNCTION =
    1.15 @@ -296,14 +296,15 @@
    1.16            CONVERSION ((arg_conv o arg1_conv o head_conv o rewr_conv) (mk_meta_eq unfold)) 1
    1.17            THEN resolve_tac lthy' @{thms refl} 1)
    1.18        end;
    1.19 +    val ((_, [rec_rule']), lthy'') = lthy' |> Local_Theory.note (eq_abinding, [rec_rule])
    1.20    in
    1.21 -    lthy'
    1.22 -    |> Local_Theory.note (eq_abinding, [rec_rule])
    1.23 -    |-> (fn (_, rec') =>
    1.24 -      Spec_Rules.add Spec_Rules.Equational ([f], rec') #> note_qualified ("simps", rec'))
    1.25 +    lthy''
    1.26 +    |> Spec_Rules.add Spec_Rules.Equational ([f], [rec_rule'])
    1.27 +    |> note_qualified ("simps", [rec_rule'])
    1.28      |> note_qualified ("mono", [mono_thm])
    1.29      |> (case raw_induct of NONE => I | SOME thm => note_qualified ("raw_induct", [thm]))
    1.30      |> note_qualified ("fixp_induct", [specialized_fixp_induct])
    1.31 +    |> pair (f, rec_rule')
    1.32    end;
    1.33  
    1.34  val add_partial_function = gen_add_partial_function Specification.check_multi_specs;
    1.35 @@ -314,6 +315,6 @@
    1.36  val _ =
    1.37    Outer_Syntax.local_theory @{command_keyword partial_function} "define partial function"
    1.38      ((mode -- (Parse.vars -- (Parse.where_ |-- Parse_Spec.simple_spec)))
    1.39 -      >> (fn (mode, (vars, spec)) => add_partial_function_cmd mode vars spec));
    1.40 +      >> (fn (mode, (vars, spec)) => add_partial_function_cmd mode vars spec #> #2));
    1.41  
    1.42  end;