# HG changeset patch
# User wenzelm
# Date 1566904953 -7200
# Node ID 7bf683f3672db858aa7702ecf6dc00a74bf68147
# Parent  7aa27d0ca431d46bf5e305081673cba3a46d314e
proper positions for 'termination' command (see also 5549e686d6ac);

diff -r 7aa27d0ca431 -r 7bf683f3672d src/HOL/Tools/Function/function.ML
--- a/src/HOL/Tools/Function/function.ML	Tue Aug 27 11:02:08 2019 +0200
+++ b/src/HOL/Tools/Function/function.ML	Tue Aug 27 13:22:33 2019 +0200
@@ -165,7 +165,7 @@
 val function = gen_function false Specification.check_multi_specs
 fun function_cmd a b c int = gen_function int Specification.read_multi_specs a b c
 
-fun prepare_termination_proof mod_binding prep_term raw_term_opt lthy =
+fun prepare_termination_proof prep_binding prep_term raw_term_opt lthy =
   let
     val term_opt = Option.map (prep_term lthy) raw_term_opt
     val info =
@@ -194,18 +194,18 @@
         val telims = map (map remove_domain_condition) pelims
       in
         lthy1
-        |> add_simps I "simps" mod_binding simp_attribs tsimps
+        |> add_simps prep_binding "simps" prep_binding simp_attribs tsimps
         ||> Code.declare_default_eqns (map (rpair true) tsimps)
         ||>> Local_Theory.note
-          ((mod_binding (derived_name defname "induct"), [Attrib.case_names case_names]), tinduct)
+          ((prep_binding (derived_name defname "induct"), [Attrib.case_names case_names]), tinduct)
         ||>> fold_map (note_derived ("elims", [Attrib.consumes 1, Attrib.constraints 1]))
-          (map mod_binding fnames ~~ telims)
+          (map prep_binding fnames ~~ telims)
         |-> (fn ((simps,(_,inducts)), elims) => fn lthy2 =>
           let val info' = { is_partial=false, defname=defname, fnames=fnames, add_simps=add_simps,
             case_names=case_names, fs=fs, R=R, dom=dom, psimps=psimps, pinducts=pinducts,
             simps=SOME simps, inducts=SOME inducts, termination=termination, totality=SOME totality,
             cases=cases, pelims=pelims, elims=SOME elims}
-            |> transform_function_data (Morphism.binding_morphism "" mod_binding)
+            |> transform_function_data (Morphism.binding_morphism "" prep_binding)
           in
             (info',
              lthy2