diff -r 22c5483e9bfb -r bf17547ce960 src/Tools/isac/Interpret/calchead.sml
--- a/src/Tools/isac/Interpret/calchead.sml	Wed May 04 09:01:10 2011 +0200
+++ b/src/Tools/isac/Interpret/calchead.sml	Wed May 04 14:04:53 2011 +0200
@@ -773,54 +773,49 @@
 fun appl_add ctxt sel [] ppc pbt ct =
       let
         val i = 1 + (if ppc = [] then 0 else map #1 ppc |> maxl);
-      in case parseNEW ctxt ct of
-          NONE => Add (i, [], false, sel, Syn ct)
-        | SOME t =>
-          let val (d, ts) = split_dts t;
-          in if d = e_term then
-            Add (i, [], false, sel, Mis (dsc_unknown, hd ts)) else
-            (case find_first (eq1 d) pbt of
-                NONE => Add (i, [], true, sel, Sup (d,ts))
-              | SOME (f, (_, id)) =>
-                let fun eq2 d (i, _, _, _, itm_) =
-                          d = (d_in itm_) andalso i <> 0;
-                in case find_first (eq2 d) ppc of
-                    NONE => Add (i, [], true, f,
-                        Cor ((d, ts), (id, pbl_ids' d ts))
-                      )
-                  | SOME (i', _, _, _, itm_) => if is_list_dsc d then
-                      let
-                        val in_itm = ts_in itm_;
-                        val ts' = union op = ts in_itm;
-                        val i'' = if in_itm = [] then i else i';
-                      in Add (i'', [], true, f,
-                          Cor ((d, ts'), (id, pbl_ids' d ts'))
-                        )
-                      end else
-                      Add (i', [], true, f, Cor ((d, ts),(id, pbl_ids' d ts)))
-                end)
-            end
+        in 
+          case parseNEW ctxt ct of
+            NONE => Add (i, [], false, sel, Syn ct)
+          | SOME t =>
+              let val (d, ts) = split_dts t;
+              in 
+                if d = e_term 
+                then Add (i, [], false, sel, Mis (dsc_unknown, hd ts)) 
+                else
+                  (case find_first (eq1 d) pbt of
+                     NONE => Add (i, [], true, sel, Sup (d,ts))
+                   | SOME (f, (_, id)) =>
+                       let fun eq2 d (i, _, _, _, itm_) =
+                             d = (d_in itm_) andalso i <> 0;
+                       in case find_first (eq2 d) ppc of
+                            NONE => Add (i, [], true, f,Cor ((d, ts), (id, pbl_ids' d ts)))
+                          | SOME (i', _, _, _, itm_) => 
+                              if is_list_dsc d 
+                              then 
+                                let
+                                  val in_itm = ts_in itm_;
+                                  val ts' = union op = ts in_itm;
+                                  val i'' = if in_itm = [] then i else i';
+                                in Add (i'', [], true, f, Cor ((d, ts'), (id, pbl_ids' d ts'))) end
+                              else Add (i', [], true, f, Cor ((d, ts),(id, pbl_ids' d ts)))
+                       end)
+              end
       end
   | appl_add ctxt sel oris ppc pbt str =
       case parseNEW ctxt str of
-          NONE => Err ("appl_add: syntax error in '" ^ str ^ "'")
-        | SOME t => case is_known ctxt sel oris t of
-            ("", ori', all) => (case is_notyet_input ctxt ppc all ori' pbt of
-              ("", itm) => Add itm
-              | (msg, _) => Err ("[error] appl_add: is_notyet_input: " ^ msg))
+        NONE => Err ("appl_add: syntax error in '" ^ str ^ "'")
+      | SOME t => 
+          case is_known ctxt sel oris t of
+            ("", ori', all) => 
+              (case is_notyet_input ctxt ppc all ori' pbt of
+                 ("", itm) => Add itm
+               | (msg, _) => Err ("[error] appl_add: is_notyet_input: " ^ msg))
           | (msg, _, _) => Err ("[error] appl_add: is_known: " ^ msg);
-(* 
-> val (msg,itm) = is_notyet_input thy ppc all ori';
-val itm = (12,[3],false,"#Relate",Cor (Const #,[#,#])) : itm
-> val itm_ = #5 itm;
-> val ts = ts_in itm_;
-> map (atomty) ts; 
-*)
+
 
 (** make oris from args of the stac SubProblem and from pbt **)
-
-(*.can this formal argument (of a model-pattern) be omitted in the arg-list
-   of a SubProblem ? see ME/ptyps.sml 'type met '.*)
+(* can this formal argument (of a model-pattern) be omitted in the arg-list
+   of a SubProblem ? see ME/ptyps.sml 'type met ' *)
 fun is_copy_named_idstr str =
     case (rev o Symbol.explode) str of
 	"'":: _ ::"'"::_ => (tracing ((strs2str o (rev o Symbol.explode))