src/HOL/Tools/ATP/atp_proof_reconstruct.ML
changeset 58652 da12763acd6b
parent 58601 85fa90262807
child 58653 4b44c227c0e0
equal deleted inserted replaced
58651:cfdd09041638 58652:da12763acd6b
   728 
   728 
   729     fun step_name_of_group skoXs = (implode skoXs, [])
   729     fun step_name_of_group skoXs = (implode skoXs, [])
   730     fun in_group group = member (op =) group o hd
   730     fun in_group group = member (op =) group o hd
   731     fun group_of skoX = find_first (fn group => in_group group skoX) groups
   731     fun group_of skoX = find_first (fn group => in_group group skoX) groups
   732 
   732 
   733     fun new_steps skoXss_steps group =
   733     fun new_steps (skoXss_steps : (string list * (term, 'a) atp_step) list) group =
   734       let
   734       let
   735         val name = step_name_of_group group
   735         val name = step_name_of_group group
   736         val name0 = name |>> prefix "0"
   736         val name0 = name |>> prefix "0"
   737         val t =
   737         val t =
   738           (case map (snd #> #3) skoXss_steps of
   738           (case map (snd #> #3) skoXss_steps of