1.1 --- a/src/Tools/isac/Interpret/calchead.sml	Thu Apr 07 16:31:05 2011 +0200
     1.2 +++ b/src/Tools/isac/Interpret/calchead.sml	Fri Apr 08 15:16:08 2011 +0200
     1.3 @@ -275,19 +275,15 @@
     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 ctxt sel (d,ts) [] =
     1.7 -    ("seek_oridts: input ('" ^ (Print_Mode.setmp [] (Syntax.string_of_term ctxt)
     1.8 -                             (comp_dts (d,ts))) ^
     1.9 -     "') not found in oris (typed)", (0, [], sel, d, ts) : ori,
    1.10 -     [])
    1.11 -  | seek_oridts ctxt sel (d,ts) ((id,vat,sel',d',ts')::(oris:ori list)) =
    1.12 -    if sel = sel' andalso d=d' andalso (inter op = ts ts') <> []
    1.13 -    then if sel = sel'
    1.14 -	 then ("", 
    1.15 -               (id,vat,sel,d, inter op = ts ts'):ori, 
    1.16 -               ts')
    1.17 -       else ((Print_Mode.setmp [] (Syntax.string_of_term ctxt) (comp_dts (d,ts)))
    1.18 -         ^ " not for " ^ sel, e_ori_, [])
    1.19 -    else seek_oridts ctxt sel (d,ts) oris;
    1.20 +    ("seek_oridts: input ('" ^
    1.21 +        (Print_Mode.setmp [] (Syntax.string_of_term ctxt) (comp_dts (d,ts))) ^
    1.22 +        "') not found in oris (typed)",
    1.23 +      (0, [], sel, d, ts),
    1.24 +      [])
    1.25 +  | seek_oridts ctxt sel (d,ts) ((id, vat, sel', d', ts')::oris) =
    1.26 +    if sel = sel' andalso d = d' andalso (inter op = ts ts') <> [] then
    1.27 +      ("", (id, vat, sel, d, inter op = ts ts'), ts') else
    1.28 +      seek_oridts ctxt sel (d, ts) oris;
    1.29  
    1.30  (*.to an input (_,ts) find the according ori and insert the ts.*)
    1.31  fun seek_orits ctxt sel ts [] = 
    1.32 @@ -774,13 +770,13 @@
    1.33  (** add an item to the model; check wrt. oris and pbt **)
    1.34  (* in contrary to oris<>[] below, this part handles user-input
    1.35     extremely acceptive, i.e. accept input instead error-msg *)
    1.36 -fun appl_add ctxt sel [] ppc pbt t =
    1.37 +fun appl_add ctxt sel [] ppc pbt ct =
    1.38        let
    1.39          val i = 1 + (if ppc = [] then 0 else map #1 ppc |> maxl);
    1.40 -      in case parse (ProofContext.theory_of ctxt) t of
    1.41 -          NONE => Add (i, [], false, sel, Syn t)
    1.42 -        | SOME t' =>
    1.43 -          let val (d, ts) = split_dts (term_of t');
    1.44 +      in case parseNEW ctxt ct of
    1.45 +          NONE => Add (i, [], false, sel, Syn ct)
    1.46 +        | SOME t =>
    1.47 +          let val (d, ts) = split_dts t;
    1.48            in if d = e_term then
    1.49              Add (i, [], false, sel, Mis (dsc_unknown, hd ts)) else
    1.50              (case find_first (eq1 d) pbt of
    1.51 @@ -811,8 +807,8 @@
    1.52          | SOME t => case is_known ctxt sel oris (term_of t) of
    1.53              ("", ori', all) => (case is_notyet_input ctxt ppc all ori' pbt of
    1.54                ("", itm) => Add itm
    1.55 -              | (msg, _) => Err msg)
    1.56 -          | (msg, _, _) => Err msg;
    1.57 +              | (msg, _) => Err ("[error] appl_add: is_notyet_input: " ^ msg))
    1.58 +          | (msg, _, _) => Err ("[error] appl_add: is_known: " ^ msg);
    1.59  (* 
    1.60  > val (msg,itm) = is_notyet_input thy ppc all ori';
    1.61  val itm = (12,[3],false,"#Relate",Cor (Const #,[#,#])) : itm