src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML
changeset 72585 18eb7ec2720f
parent 72584 4ea19e5dc67e
equal deleted inserted replaced
72584:4ea19e5dc67e 72585:18eb7ec2720f
   206   | chain_isar_step _ step = step
   206   | chain_isar_step _ step = step
   207 and chain_isar_steps _ [] = []
   207 and chain_isar_steps _ [] = []
   208   | chain_isar_steps prev (i :: is) =
   208   | chain_isar_steps prev (i :: is) =
   209     chain_isar_step prev i :: chain_isar_steps (label_of_isar_step i) is
   209     chain_isar_step prev i :: chain_isar_steps (label_of_isar_step i) is
   210 and chain_isar_proof (proof as Proof {assumptions, steps, ...}) =
   210 and chain_isar_proof (proof as Proof {assumptions, steps, ...}) =
   211     isar_proof_with_steps proof (chain_isar_steps (try (List.last #> fst) assumptions) steps)
   211   isar_proof_with_steps proof (chain_isar_steps (try (List.last #> fst) assumptions) steps)
   212 
   212 
   213 fun kill_useless_labels_in_isar_proof proof =
   213 fun kill_useless_labels_in_isar_proof proof =
   214   let
   214   let
   215     val used_ls =
   215     val used_ls =
   216       fold_isar_steps (facts_of_isar_step #> fst #> union (op =)) (steps_of_isar_proof proof) []
   216       fold_isar_steps (facts_of_isar_step #> fst #> union (op =)) (steps_of_isar_proof proof) []