1.1 --- a/TFL/post.ML	Thu Sep 02 11:29:06 2004 +0200
     1.2 +++ b/TFL/post.ML	Thu Sep 02 14:50:00 2004 +0200
     1.3 @@ -203,7 +203,8 @@
     1.4  together and say that they must be true to solve the general case,
     1.5  but that would hide from the user which sub-case they were related
     1.6  to. Probably this is not important, and it would work fine, but, for now, I
     1.7 -prefer leaving more fine-grain control to the user. *)
     1.8 +prefer leaving more fine-grain control to the user. 
     1.9 +-- Lucas Dixon, Aug 2004 *)
    1.10  local
    1.11    fun get_related_thms i = 
    1.12        mapfilter ((fn (r,x) => if x = i then Some r else None));
    1.13 @@ -212,11 +213,13 @@
    1.14        raise ERROR_MESSAGE "derive_init_eqs: missing rules"
    1.15      | solve_eq (th, [a], i) = [(a, i)]
    1.16      | solve_eq (th, splitths as (_ :: _), i) = 
    1.17 +      (writeln "Proving unsplit equation...";
    1.18        [((standard o ObjectLogic.rulify_no_asm)
    1.19 -          (CaseSplit.splitto splitths th), i)]
    1.20 +          (CaseSplit.splitto splitths th), i)])
    1.21        (* if there's an error, pretend nothing happened with this definition 
    1.22           We should probably print something out so that the user knows...? *)
    1.23 -      handle ERROR_MESSAGE _ => map (fn x => (x,i)) splitths; 
    1.24 +      handle ERROR_MESSAGE s => 
    1.25 +             (writeln ("WARNING:post.ML:solve_eq: " ^ s); map (fn x => (x,i)) splitths); 
    1.26  in
    1.27  fun derive_init_eqs sgn rules eqs = 
    1.28      let 
    1.29 @@ -237,7 +240,12 @@
    1.30  fun define_i strict thy cs ss congs wfs fid R eqs =
    1.31    let val {functional,pats} = Prim.mk_functional thy eqs
    1.32        val (thy, def) = Prim.wfrec_definition0 thy (Sign.base_name fid) R functional
    1.33 -  in (thy, simplify_defn strict thy cs ss congs wfs fid pats def) end;
    1.34 +      val {induct, rules, tcs} = 
    1.35 +          simplify_defn strict thy cs ss congs wfs fid pats def
    1.36 +      val rules' = 
    1.37 +          if strict then derive_init_eqs (Theory.sign_of thy) rules eqs
    1.38 +          else rules
    1.39 +  in (thy, {rules = rules', induct = induct, tcs = tcs}) end;
    1.40  
    1.41  fun define strict thy cs ss congs wfs fid R seqs =
    1.42    define_i strict thy cs ss congs wfs fid (read_term thy R) (map (read_term thy) seqs)