equal
deleted
inserted
replaced
178 #> apfst (apsnd snd) |
178 #> apfst (apsnd snd) |
179 |
179 |
180 val (updates, (lthy'', lthy')) = |
180 val (updates, (lthy'', lthy')) = |
181 lthy |
181 lthy |
182 |> Local_Theory.open_target |
182 |> Local_Theory.open_target |
183 |> snd |
|
184 |> Local_Theory.map_background_naming (Name_Space.qualified_path false (Binding.name short_name)) |
183 |> Local_Theory.map_background_naming (Name_Space.qualified_path false (Binding.name short_name)) |
185 |> @{fold_map 2} define (map mk_name sels) (Syntax.check_terms lthy (map mk_t (0 upto len - 1))) |
184 |> @{fold_map 2} define (map mk_name sels) (Syntax.check_terms lthy (map mk_t (0 upto len - 1))) |
186 ||> `Local_Theory.close_target |
185 ||> `Local_Theory.close_target |
187 |
186 |
188 val phi = Proof_Context.export_morphism lthy' lthy'' |
187 val phi = Proof_Context.export_morphism lthy' lthy'' |