1.1 --- a/src/Tools/isac/Interpret/calchead.sml	Thu Mar 17 10:46:02 2011 +0100
     1.2 +++ b/src/Tools/isac/Interpret/calchead.sml	Fri Mar 18 09:26:03 2011 +0100
     1.3 @@ -278,9 +278,9 @@
     1.4  (*.to an input (d,ts) find the according ori and insert the ts.*)
     1.5  (*WN.11.03: + dont take first inter<>[]*)
     1.6  fun seek_oridts thy sel (d,ts) [] = 
     1.7 -    ("'" ^ (Print_Mode.setmp [] (Syntax.string_of_term (thy2ctxt thy))
     1.8 +    ("seek_oridts: input ('" ^ (Print_Mode.setmp [] (Syntax.string_of_term (thy2ctxt thy))
     1.9                               (comp_dts thy (d,ts))) ^
    1.10 -     "' not found (typed)", (0, [], sel, d, ts) : ori,
    1.11 +     "') not found in oris (typed)", (0, [], sel, d, ts) : ori,
    1.12       [])
    1.13    | seek_oridts thy sel (d,ts) ((id,vat,sel',d',ts')::(oris:ori list)) =
    1.14      if sel = sel' andalso d=d' andalso (inter op = ts ts') <> [] 
    1.15 @@ -296,9 +296,9 @@
    1.16  
    1.17  (*.to an input (_,ts) find the according ori and insert the ts.*)
    1.18  fun seek_orits thy sel ts [] = 
    1.19 -  ("'" ^ strs2str (map (Print_Mode.setmp [](Syntax.string_of_term 
    1.20 +  ("seek_orits: input (_, '" ^ strs2str (map (Print_Mode.setmp [](Syntax.string_of_term 
    1.21                                             (thy2ctxt thy))) ts) ^
    1.22 -   "' not found (typed)", e_ori_, [])
    1.23 +   "') not found in oris (typed)", e_ori_, [])
    1.24    | seek_orits thy sel ts ((id,vat,sel',d,ts')::(oris:ori list)) =
    1.25      if sel = sel' andalso (inter op = ts ts') <> [] 
    1.26      then if sel = sel' 
    1.27 @@ -740,6 +740,7 @@
    1.28  (* val (ori,t)=(oris,term_of ct);
    1.29     *)
    1.30    let
    1.31 +    val _ = tracing ("RM is_known: t=" ^ term2str t);
    1.32      val ots = (distinct o flat o (map #5)) (ori:ori list);
    1.33      val oids = ((map (fst o dest_Free)) o distinct o 
    1.34  		flat o (map vars)) ots;