1.1 --- a/src/HOL/Tools/TFL/post.ML	Fri Mar 04 11:52:54 2011 +0100
     1.2 +++ b/src/HOL/Tools/TFL/post.ML	Fri Mar 04 11:43:20 2011 +0100
     1.3 @@ -161,38 +161,24 @@
     1.4  
     1.5  
     1.6  (* Derive the initial equations from the case-split rules to meet the
     1.7 -users specification of the recursive function. 
     1.8 - Note: We don't do this if the wf conditions fail to be solved, as each
     1.9 -case may have a different wf condition. We could group the conditions
    1.10 -together and say that they must be true to solve the general case,
    1.11 -but that would hide from the user which sub-case they were related
    1.12 -to. Probably this is not important, and it would work fine, but, for now, I
    1.13 -prefer leaving more fine-grain control to the user. 
    1.14 --- Lucas Dixon, Aug 2004 *)
    1.15 +users specification of the recursive function. *)
    1.16  local
    1.17    fun get_related_thms i = 
    1.18        map_filter ((fn (r,x) => if x = i then SOME r else NONE));
    1.19  
    1.20 -  fun solve_eq (th, [], i) = 
    1.21 -        error "derive_init_eqs: missing rules"
    1.22 +  fun solve_eq (th, [], i) =  error "derive_init_eqs: missing rules"
    1.23      | solve_eq (th, [a], i) = [(a, i)]
    1.24 -    | solve_eq (th, splitths as (_ :: _), i) = 
    1.25 +    | solve_eq (th, splitths, i) =
    1.26        (writeln "Proving unsplit equation...";
    1.27        [((Drule.export_without_context o Object_Logic.rulify_no_asm)
    1.28            (CaseSplit.splitto splitths th), i)])
    1.29 -      (* if there's an error, pretend nothing happened with this definition 
    1.30 -         We should probably print something out so that the user knows...? *)
    1.31        handle ERROR s => 
    1.32               (warning ("recdef (solve_eq): " ^ s); map (fn x => (x,i)) splitths);
    1.33  in
    1.34 -fun derive_init_eqs sgn rules eqs = 
    1.35 -    let 
    1.36 -      val eqths = map (Thm.trivial o (Thm.cterm_of sgn) o HOLogic.mk_Trueprop) eqs
    1.37 -      fun countlist l =
    1.38 -        rev (snd (fold (fn e => fn (i, L) => (i + 1, (e, i) :: L)) l (0, [])))
    1.39 -    in
    1.40 -      maps (fn (e, i) => solve_eq (e, (get_related_thms i rules), i)) (countlist eqths)
    1.41 -    end;
    1.42 +fun derive_init_eqs thy rules eqs =
    1.43 +  map (Thm.trivial o Thm.cterm_of thy o HOLogic.mk_Trueprop) eqs
    1.44 +  |> map_index (fn (i, e) => solve_eq (e, (get_related_thms i rules), i))
    1.45 +  |> flat;
    1.46  end;
    1.47  
    1.48