1.1 --- a/src/Tools/isac/calcelems.sml	Thu Nov 24 14:33:42 2016 +0100
     1.2 +++ b/src/Tools/isac/calcelems.sml	Wed Nov 30 12:09:24 2016 +0100
     1.3 @@ -285,11 +285,12 @@
     1.4  fun Isac _ = Proof_Context.theory_of (thy2ctxt' "Isac"); (*@{theory "Isac"}*)
     1.5                                       
     1.6  val e_rule = Thm ("refl", @{thm refl});
     1.7 -fun id_of_thm (Thm (id, _)) = id
     1.8 -  | id_of_thm _ = error "error id_of_thm";
     1.9 -fun thm_of_thm (Thm (_, thm)) = thm
    1.10 -  | thm_of_thm _ = error "error thm_of_thm";
    1.11 -fun rep_thm_G' (Thm (thmid, thm)) = (thmid, thm);
    1.12 +fun id_of_thm (Thm (id, _)) = id  (* TODO re-arrange code for rule2str *)
    1.13 +  | id_of_thm _ = raise ERROR ("id_of_thm: uncovered case " (* ^ rule2str r *))
    1.14 +fun thm_of_thm (Thm (_, thm)) = thm  (* TODO re-arrange code for rule2str *)
    1.15 +  | thm_of_thm _ = raise ERROR ("thm_of_thm: uncovered case " (* ^ rule2str r *))
    1.16 +fun rep_thm_G' (Thm (thmid, thm)) = (thmid, thm)  (* TODO re-arrange code for rule2str *)
    1.17 +  | rep_thm_G' _ = raise ERROR ("rep_thm_G': uncovered case " (* ^ rule2str r *))
    1.18  
    1.19  fun thmID_of_derivation_name dn = last_elem (space_explode "." dn);
    1.20  fun thmID_of_derivation_name' thm = (thmID_of_derivation_name o Thm.get_name_hint) thm