TFL/post.ML
changeset 16852 b950180e243d
parent 16287 7a03b4b4df67
child 16975 34ed8d5d4f16
equal deleted inserted replaced
16851:551462cc8ca0 16852:b950180e243d
   131   in
   131   in
   132   case nested_tcs
   132   case nested_tcs
   133   of [] => {induction=induction, rules=rules,tcs=[]}
   133   of [] => {induction=induction, rules=rules,tcs=[]}
   134   | L  => let val dummy = message "Simplifying nested TCs ..."
   134   | L  => let val dummy = message "Simplifying nested TCs ..."
   135               val (solved,simplified,stubborn) =
   135               val (solved,simplified,stubborn) =
   136                U.itlist (fn th => fn (So,Si,St) =>
   136                fold_rev (fn th => fn (So,Si,St) =>
   137                      if (id_thm th) then (So, Si, th::St) else
   137                      if (id_thm th) then (So, Si, th::St) else
   138                      if (solved th) then (th::So, Si, St)
   138                      if (solved th) then (th::So, Si, St)
   139                      else (So, th::Si, St)) nested_tcs ([],[],[])
   139                      else (So, th::Si, St)) nested_tcs ([],[],[])
   140               val simplified' = map join_assums simplified
   140               val simplified' = map join_assums simplified
   141               val dummy = (Prim.trace_thms "solved =" solved;
   141               val dummy = (Prim.trace_thms "solved =" solved;