1.1 --- a/src/Tools/isac/calcelems.sml	Wed Jan 22 15:31:35 2014 +0100
     1.2 +++ b/src/Tools/isac/calcelems.sml	Wed Jan 22 15:47:14 2014 +0100
     1.3 @@ -793,8 +793,15 @@
     1.4  
     1.5  val e_pbt = {guh = "pbl_empty", mathauthors = [], init = e_pblID, thy = Thy_Info.get_theory "Pure",
     1.6    cas = NONE, prls = Erls, where_ = [], ppc = [], met = []} : pbt
     1.7 -fun pbt2 (str, (t1, t2)) = pair2str (str, pair2str (term2str t1, term2str t2))
     1.8 -fun pbt2str pbt = (strs2str o (map (linefeed o pbt2))) pbt
     1.9 +fun pbt2str
    1.10 +        ({cas = cas', guh = guh', init = init', mathauthors = ma', met = met', ppc = ppc',
    1.11 +          prls = prls', thy = thy', where_ = where'} : pbt) =
    1.12 +      "{cas = " ^ (termopt2str cas') ^  ", guh = \"" ^ guh'  ^ "\", init = "
    1.13 +      ^ (strs2str init') ^ ", mathauthors = \"" ^ (strs2str ma') ^ "\", met = "
    1.14 +      ^ (strslist2strs met') ^ ", ppc = " ^ pats2str ppc' ^ ", prls = \""
    1.15 +      ^ (rls2str prls') ^ "\", thy = {" ^ Context.theory_name thy'
    1.16 +      ^ "}, where_ = " ^ (terms2str where') ^ "}" |> linefeed;
    1.17 +fun pbts2str pbts = map pbt2str pbts |> strs2str;
    1.18  
    1.19  val e_Ptyp = Ptyp ("e_pblID",[e_pbt],[])
    1.20  type ptyps = (pbt ptyp) list