equal
deleted
inserted
replaced
391 resTs (map (Binding.suffix_name ("_" ^ un_foldN)) bs) (([], []), (empty_cache, lthy)) |
391 resTs (map (Binding.suffix_name ("_" ^ un_foldN)) bs) (([], []), (empty_cache, lthy)) |
392 |>> map_prod rev rev |
392 |>> map_prod rev rev |
393 |>> pair ss |
393 |>> pair ss |
394 end; |
394 end; |
395 val ((ss, (un_folds, un_fold_defs0)), (cache, (lthy, raw_lthy))) = lthy |
395 val ((ss, (un_folds, un_fold_defs0)), (cache, (lthy, raw_lthy))) = lthy |
396 |> Local_Theory.open_target |> snd |
396 |> Local_Theory.open_target |
397 |> Variable.add_fixes (mk_names n "s") |
397 |> Variable.add_fixes (mk_names n "s") |
398 |> mk_un_folds |
398 |> mk_un_folds |
399 ||> apsnd (`(Local_Theory.close_target)); |
399 ||> apsnd (`(Local_Theory.close_target)); |
400 |
400 |
401 val un_fold_defs = map (unfold_thms raw_lthy @{thms Let_const}) un_fold_defs0; |
401 val un_fold_defs = map (unfold_thms raw_lthy @{thms Let_const}) un_fold_defs0; |