# HG changeset patch
# User wenzelm
# Date 1566764244 -7200
# Node ID 5549e686d6acb1475d9e8f52186a3f348dcb35ce
# Parent  d997c7ba3305cc61644aa40d0a277bc29242f787
proper positions for 'termination' command instead of original 'function' command, e.g. relevant for isabelle mmt_import;

diff -r d997c7ba3305 -r 5549e686d6ac src/HOL/Tools/Function/function.ML
--- a/src/HOL/Tools/Function/function.ML	Sat Aug 24 12:03:00 2019 +0200
+++ b/src/HOL/Tools/Function/function.ML	Sun Aug 25 22:17:24 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 prep_term raw_term_opt lthy =
+fun prepare_termination_proof mod_binding prep_term raw_term_opt lthy =
   let
     val term_opt = Option.map (prep_term lthy) raw_term_opt
     val info =
@@ -194,17 +194,18 @@
         val telims = map (map remove_domain_condition) pelims
       in
         lthy
-        |> add_simps I "simps" I simp_attribs tsimps
+        |> add_simps I "simps" mod_binding simp_attribs tsimps
         ||> Code.declare_default_eqns (map (rpair true) tsimps)
         ||>> Local_Theory.note
-          ((derived_name defname "induct", [Attrib.case_names case_names]), tinduct)
+          ((mod_binding (derived_name defname "induct"), [Attrib.case_names case_names]), tinduct)
         ||>> fold_map (note_derived ("elims", [Attrib.consumes 1, Attrib.constraints 1]))
-          (fnames ~~ telims)
+          (map mod_binding fnames ~~ telims)
         |-> (fn ((simps,(_,inducts)), elims) => fn lthy =>
           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)
           in
             (info',
              lthy
@@ -220,7 +221,7 @@
 fun gen_prove_termination prep_term raw_term_opt tac lthy =
   let
     val (goal, afterqed, termination) =
-      prepare_termination_proof prep_term raw_term_opt lthy
+      prepare_termination_proof I prep_term raw_term_opt lthy
 
     val totality = Goal.prove lthy [] [] goal (K tac)
   in
@@ -232,7 +233,8 @@
 
 fun gen_termination prep_term raw_term_opt lthy =
   let
-    val (goal, afterqed, termination) = prepare_termination_proof prep_term raw_term_opt lthy
+    val (goal, afterqed, termination) =
+      prepare_termination_proof Binding.reset_pos prep_term raw_term_opt lthy
   in
     lthy
     |> Proof_Context.note_thms ""