1.1 --- a/src/Tools/isac/calcelems.sml	Mon Sep 02 15:17:34 2013 +0200
     1.2 +++ b/src/Tools/isac/calcelems.sml	Mon Sep 02 16:16:08 2013 +0200
     1.3 @@ -97,7 +97,7 @@
     1.4  and scr =
     1.5      EmptyScr
     1.6    | Prog of term (* for met *)
     1.7 -  | Rfuns of     (* for Rrls*)
     1.8 +  | Rfuns of     (* for Rrls, usage see rational.sml ----- reverse rewrite -----      *)
     1.9      {init_state : (* initialise for reverse rewriting by the Interpreter              *)
    1.10        term ->         (* for this the rrlsstate is initialised:                       *)
    1.11        term *          (* the current formula: goes locate_gen -> next_tac via istate  *)
    1.12 @@ -194,9 +194,9 @@
    1.13                                       
    1.14  val e_rule = Thm ("refl", @{thm refl});
    1.15  fun id_of_thm (Thm (id, _)) = id
    1.16 -  | id_of_thm _ = error "id_of_thm";
    1.17 +  | id_of_thm _ = error "error id_of_thm";
    1.18  fun thm_of_thm (Thm (_, thm)) = thm
    1.19 -  | thm_of_thm _ = error "thm_of_thm";
    1.20 +  | thm_of_thm _ = error "error thm_of_thm";
    1.21  fun rep_thm_G' (Thm (thmid, thm)) = (thmid, thm);
    1.22  
    1.23  fun thmID_of_derivation_name dn = last_elem (space_explode "." dn);