TFL/post.ML
changeset 17615 3c5b158be33c
parent 16975 34ed8d5d4f16
child 17959 8db36a108213
equal deleted inserted replaced
17614:37ee526db497 17615:3c5b158be33c
   214       [((standard o ObjectLogic.rulify_no_asm)
   214       [((standard o ObjectLogic.rulify_no_asm)
   215           (CaseSplit.splitto splitths th), i)])
   215           (CaseSplit.splitto splitths th), i)])
   216       (* if there's an error, pretend nothing happened with this definition 
   216       (* if there's an error, pretend nothing happened with this definition 
   217          We should probably print something out so that the user knows...? *)
   217          We should probably print something out so that the user knows...? *)
   218       handle ERROR_MESSAGE s => 
   218       handle ERROR_MESSAGE s => 
   219              (writeln ("WARNING:post.ML:solve_eq: " ^ s); map (fn x => (x,i)) splitths); 
   219              (warning ("recdef (solve_eq): " ^ s); map (fn x => (x,i)) splitths);
   220 in
   220 in
   221 fun derive_init_eqs sgn rules eqs = 
   221 fun derive_init_eqs sgn rules eqs = 
   222     let 
   222     let 
   223       val eqths = map (Thm.trivial o (Thm.cterm_of sgn) o HOLogic.mk_Trueprop) 
   223       val eqths = map (Thm.trivial o (Thm.cterm_of sgn) o HOLogic.mk_Trueprop) 
   224                       eqs
   224                       eqs