372 let |
372 let |
373 val (parm_names, parm_types) = Locale.params_types_of thy loc; |
373 val (parm_names, parm_types) = Locale.params_types_of thy loc; |
374 val inst' = prep_inst ctxt parm_names inst; |
374 val inst' = prep_inst ctxt parm_names inst; |
375 val eqns' = map (apsnd (parse_eqn ctxt)) eqns; |
375 val eqns' = map (apsnd (parse_eqn ctxt)) eqns; |
376 val parm_types' = parm_types |
376 val parm_types' = parm_types |
377 |> map (Type_Infer.paramify_vars o |
377 |> map (Logic.varifyT_global #> |
378 Term.map_type_tvar (fn ((x, _), S) => TVar ((x, i), S)) o Logic.varifyT_global); |
378 Term.map_type_tvar (fn ((x, _), S) => TVar ((x, i), S)) #> |
|
379 Type_Infer.paramify_vars); |
379 val inst'' = map2 Type.constraint parm_types' inst'; |
380 val inst'' = map2 Type.constraint parm_types' inst'; |
380 val insts' = insts @ [(loc, (prfx, inst''))]; |
381 val insts' = insts @ [(loc, (prfx, inst''))]; |
381 val eqnss' = eqnss @ [eqns']; |
382 val eqnss' = eqnss @ [eqns']; |
382 val ((insts'', eqnss'', _, _), _) = check_autofix insts' eqnss' [] [] ctxt; |
383 val ((insts'', eqnss'', _, _), _) = check_autofix insts' eqnss' [] [] ctxt; |
383 val inst''' = insts'' |> List.last |> snd |> snd; |
384 val (inst_morph, _) = |
384 val eqns'' = eqnss'' |> List.last; |
385 inst_morphism (parm_names, parm_types) (prfx, #2 (#2 (List.last insts''))) ctxt; |
385 val (inst_morph, _) = inst_morphism (parm_names, parm_types) (prfx, inst''') ctxt; |
386 val rewrite_morph = |
386 val rewrite_morph = eqns'' |> map (snd #> Thm.cterm_of ctxt #> Thm.assume #> Local_Defs.abs_def_rule ctxt) |> |
387 List.last eqnss'' |
387 Element.eq_morphism (Proof_Context.theory_of ctxt) |> the_default Morphism.identity; |
388 |> map (snd #> Thm.cterm_of ctxt #> Thm.assume #> Local_Defs.abs_def_rule ctxt) |
388 val ctxt'' = Locale.activate_declarations (loc, inst_morph $> rewrite_morph) ctxt; |
389 |> Element.eq_morphism (Proof_Context.theory_of ctxt) |
389 in (i + 1, insts', eqnss', ctxt'') end; |
390 |> the_default Morphism.identity; |
|
391 val ctxt' = Locale.activate_declarations (loc, inst_morph $> rewrite_morph) ctxt; |
|
392 in (i + 1, insts', eqnss', ctxt') end; |
390 |
393 |
391 fun prep_elem raw_elem ctxt = |
394 fun prep_elem raw_elem ctxt = |
392 let |
395 let |
393 val ctxt' = ctxt |
396 val ctxt' = ctxt |
394 |> Context_Position.set_visible false |
397 |> Context_Position.set_visible false |