1.1 --- a/src/Tools/isac/Interpret/inform.sml	Sun Jul 21 15:15:50 2013 +0200
     1.2 +++ b/src/Tools/isac/Interpret/inform.sml	Mon Jul 22 13:52:18 2013 +0200
     1.3 @@ -200,36 +200,40 @@
     1.4  
     1.5  (*re-parse itms with a new thy and prepare for checking with ori list*)
     1.6  fun parsitm dI (itm as (i,v,b,f, Cor ((d,ts),_)):itm) =
     1.7 -(* val itm as (i,v,b,f, Cor ((d,ts),_)) = hd probl;
     1.8 -   *)
     1.9 -    (let val t = comp_dts (d,ts);
    1.10 -	 val s = Print_Mode.setmp [] (Syntax.string_of_term (thy2ctxt dI)) t;
    1.11 -     (*this    ^ should raise the exn on unability of re-parsing dts*)
    1.12 -     in itm end handle _ => ((i,v,false,f, Syn (term2str t)):itm))
    1.13 +    (let
    1.14 +      val t = comp_dts (d,ts);
    1.15 +      val s = term_to_string''' dI t;
    1.16 +       (*this    ^ should raise the exn on unability of re-parsing dts*)
    1.17 +    in itm end
    1.18 +    handle _ => ((i,v,false,f, Syn (term2str t)):itm))
    1.19    | parsitm dI (itm as (i,v,b,f, Syn str)) =
    1.20      (let val t = (term_of o the o (parse dI)) str
    1.21 -     in (i,v,b,f, Par str) end handle _ => (i,v,b,f, Syn str))
    1.22 +    in (i,v,b,f, Par str) end
    1.23 +    handle _ => (i,v,b,f, Syn str))
    1.24    | parsitm dI (itm as (i,v,b,f, Typ str)) =
    1.25      (let val t = (term_of o the o (parse dI)) str
    1.26 -     in (i,v,b,f, Par str) end handle _ => (i,v,b,f, Syn str))
    1.27 +     in (i,v,b,f, Par str) end
    1.28 +     handle _ => (i,v,b,f, Syn str))
    1.29    | parsitm dI (itm as (i,v,_,f, Inc ((d,ts),_))) =
    1.30      (let val t = comp_dts (d,ts);
    1.31 -	 val s = Print_Mode.setmp [] (Syntax.string_of_term (thy2ctxt dI)) t;
    1.32 +	       val s = term_to_string''' dI t;
    1.33       (*this    ^ should raise the exn on unability of re-parsing dts*)
    1.34 -     in itm end handle _ => ((i,v,false,f, Syn (term2str t)):itm))
    1.35 +     in itm end
    1.36 +     handle _ => ((i,v,false,f, Syn (term2str t)):itm))
    1.37    | parsitm dI (itm as (i,v,_,f, Sup (d,ts))) =
    1.38      (let val t = comp_dts (d,ts);
    1.39 -	 val s = Print_Mode.setmp [] (Syntax.string_of_term (thy2ctxt dI)) t;
    1.40 +	       val s = term_to_string''' dI t;
    1.41       (*this    ^ should raise the exn on unability of re-parsing dts*)
    1.42 -     in itm end handle _ => ((i,v,false,f, Syn (term2str t)):itm))
    1.43 +    in itm end
    1.44 +    handle _ => ((i,v,false,f, Syn (term2str t)):itm))
    1.45    | parsitm dI (itm as (i,v,_,f, Mis (d,t'))) =
    1.46      (let val t = d $ t';
    1.47 -	 val s = Print_Mode.setmp [] (Syntax.string_of_term (thy2ctxt dI)) t;
    1.48 +	       val s = term_to_string''' dI t;
    1.49       (*this    ^ should raise the exn on unability of re-parsing dts*)
    1.50 -     in itm end handle _ => ((i,v,false,f, Syn (term2str t)):itm))
    1.51 +    in itm end
    1.52 +    handle _ => ((i,v,false,f, Syn (term2str t)):itm))
    1.53    | parsitm dI (itm as (i,v,_,f, Par _)) = 
    1.54 -    error ("parsitm (" ^ itm2str_ (thy2ctxt dI) itm^
    1.55 -		 "): Par should be internal");
    1.56 +    error ("parsitm (" ^ itm2str_ (thy2ctxt dI) itm ^ "): Par should be internal");
    1.57  
    1.58  (*separate a list to a pair of elements that do NOT satisfy the predicate,
    1.59   and of elements that satisfy the predicate, i.e. (false, true)*)