86 ||> (snd o note_theorem ((qualify "cases", []), [cases])) |
86 ||> (snd o note_theorem ((qualify "cases", []), [cases])) |
87 ||> fold_option (snd oo curry note_theorem (qualify "domintros", [])) domintros |
87 ||> fold_option (snd oo curry note_theorem (qualify "domintros", [])) domintros |
88 |
88 |
89 val cdata = FundefCtxData { add_simps=addsmps, psimps=psimps', |
89 val cdata = FundefCtxData { add_simps=addsmps, psimps=psimps', |
90 pinducts=snd pinducts', termination=termination', f=f, R=R } |
90 pinducts=snd pinducts', termination=termination', f=f, R=R } |
91 |> morph_fundef_data (LocalTheory.target_morphism lthy) |
91 val cdata' = cdata |> morph_fundef_data (LocalTheory.target_morphism lthy); (* FIXME !? *) |
92 in |
92 in |
93 lthy |
93 lthy |
94 |> LocalTheory.declaration (fn phi => add_fundef_data defname (morph_fundef_data phi cdata)) (* save in target *) |
94 |> LocalTheory.declaration (fn phi => add_fundef_data defname (morph_fundef_data phi cdata)) (* save in target *) |
95 |> Context.proof_map (add_fundef_data defname cdata) (* also save in local context *) |
95 |> Context.proof_map (add_fundef_data defname cdata') (* also save in local context *) |
96 end (* FIXME: Add cases for induct and cases thm *) |
96 end (* FIXME: Add cases for induct and cases thm *) |
97 |
97 |
98 |
98 |
99 |
99 |
100 fun prep_with_flags prep fixspec eqnss_flags global_flag lthy = |
100 fun prep_with_flags prep fixspec eqnss_flags global_flag lthy = |